Proof of proveit.physics.quantum.QPE.main_theorems_combined theorem

import proveit
theory = proveit.Theory() # the theorem's theory

from proveit.physics.quantum.QPE import qpe_exact, qpe_best_guarantee, qpe_precision_guarantee

%proving main_theorems_combined

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
main_theorems_combined:
(see dependencies)

main_theorems_combined may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.physics.quantum.QPE.main_theorems_combined has been proven.

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5, 6	⊢
	: , :
1	conjecture		⊢
	proveit.logic.booleans.conjunction.and_if_all
2	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
3	instantiation	7	⊢
	: , : , :
4	conjecture		⊢
	proveit.physics.quantum.QPE.qpe_exact
5	conjecture		⊢
	proveit.physics.quantum.QPE.qpe_best_guarantee
6	conjecture		⊢
	proveit.physics.quantum.QPE.qpe_precision_guarantee
7	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq