Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	reference	178	⊢
2	instantiation	4, 5, 6	⊢
	: , : , :
3	instantiation	7, 217	⊢
	:
4	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
5	instantiation	106, 12, 8, 11, 9	⊢
	: , : , :
6	instantiation	10, 11, 12, 13, 14	⊢
	: , : , :
7	theorem		⊢
	proveit.physics.quantum.QPE._fail_sum
8	modus ponens	15, 16	⊢
9	modus ponens	17, 18	⊢
10	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
11	modus ponens	19, 20	⊢
12	modus ponens	21, 22	⊢
13	modus ponens	23, 24	⊢
14	modus ponens	25, 26	⊢
15	instantiation	31	⊢
	: , : , :
16	generalization	27	⊢
17	instantiation	33	⊢
	: , : , :
18	generalization	28	⊢
19	instantiation	31	⊢
	: , : , :
20	generalization	29	⊢
21	instantiation	31	⊢
	: , : , :
22	generalization	30	⊢
23	instantiation	31	⊢
	: , : , :
24	generalization	32	⊢
25	instantiation	33	⊢
	: , : , :
26	generalization	34	⊢
27	instantiation	66, 35, 243	,  ⊢
	: , :
28	instantiation	43, 36, 112	,  ⊢
	:
29	instantiation	40, 222, 37, 38	,  ⊢
	: , :
30	instantiation	66, 39, 243	,  ⊢
	: , :
31	theorem		⊢
	proveit.numbers.summation.summation_real_closure
32	instantiation	40, 222, 41, 42	,  ⊢
	: , :
33	theorem		⊢
	proveit.numbers.summation.weak_summation_from_summands_bound
34	instantiation	43, 44, 117	,  ⊢
	:
35	instantiation	244, 49, 45	,  ⊢
	: , : , :
36	instantiation	57, 154, 227, 123, 46	,  ⊢
	: , : , :
37	instantiation	126, 51, 47	,  ⊢
	: , :
38	instantiation	53, 243, 54, 55, 48	,  ⊢
	: , :
39	instantiation	244, 49, 50	,  ⊢
	: , : , :
40	theorem		⊢
	proveit.numbers.division.div_real_closure
41	instantiation	126, 51, 52	,  ⊢
	: , :
42	instantiation	53, 243, 54, 55, 56	,  ⊢
	: , :
43	theorem		⊢
	proveit.physics.quantum.QPE._alpha_sqrd_upper_bound
44	instantiation	57, 154, 227, 145, 58	,  ⊢
	: , : , :
45	instantiation	63, 59	,  ⊢
	:
46	instantiation	71, 60, 61	,  ⊢
	: , :
47	instantiation	66, 89, 243	,  ⊢
	: , :
48	instantiation	69, 62, 196	,  ⊢
	: , :
49	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
50	instantiation	63, 64	,  ⊢
	:
51	instantiation	244, 231, 65	⊢
	: , : , :
52	instantiation	66, 94, 243	,  ⊢
	: , :
53	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
54	instantiation	67	⊢
	: , :
55	instantiation	244, 212, 68	⊢
	: , : , :
56	instantiation	69, 70, 196	,  ⊢
	: , :
57	theorem		⊢
	proveit.numbers.number_sets.integers.in_interval
58	instantiation	71, 72, 73	,  ⊢
	: , :
59	instantiation	78, 74	,  ⊢
	:
60	instantiation	215, 154, 155, 156	,  ⊢
	: , : , :
61	instantiation	85, 75	,  ⊢
	: , :
62	instantiation	82, 76, 77	,  ⊢
	:
63	theorem		⊢
	proveit.numbers.absolute_value.abs_complex_closure
64	instantiation	78, 79	,  ⊢
	:
65	instantiation	244, 239, 80	⊢
	: , : , :
66	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
67	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
68	instantiation	244, 224, 81	⊢
	: , : , :
69	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_nonzero_closure
70	instantiation	82, 83, 84	,  ⊢
	:
71	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
72	instantiation	85, 86	,  ⊢
	: , :
73	instantiation	153, 171, 227, 172	,  ⊢
	: , : , :
74	instantiation	91, 144, 123	,  ⊢
	: , :
75	instantiation	87, 125, 88	,  ⊢
	: , : , :
76	instantiation	244, 221, 89	,  ⊢
	: , : , :
77	instantiation	95, 90	,  ⊢
	: , :
78	theorem		⊢
	proveit.physics.quantum.QPE._alpha_are_complex
79	instantiation	91, 144, 145	,  ⊢
	: , :
80	instantiation	244, 245, 92	⊢
	: , : , :
81	instantiation	244, 233, 93	⊢
	: , : , :
82	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
83	instantiation	244, 221, 94	,  ⊢
	: , : , :
84	instantiation	95, 96	,  ⊢
	: , :
85	theorem		⊢
	proveit.numbers.ordering.relax_less
86	instantiation	140, 97, 146	,  ⊢
	: , : , :
87	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
88	instantiation	169, 236	⊢
	:
89	instantiation	101, 98, 103	,  ⊢
	: , :
90	instantiation	104, 99	,  ⊢
	: , :
91	theorem		⊢
	proveit.physics.quantum.QPE._mod_add_closure
92	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
93	instantiation	244, 241, 100	⊢
	: , : , :
94	instantiation	101, 102, 103	,  ⊢
	: , :
95	theorem		⊢
	proveit.numbers.addition.subtraction.nonzero_difference_if_different
96	instantiation	104, 105	,  ⊢
	: , :
97	instantiation	106, 132, 222, 107, 108, 109*, 110*	⊢
	: , : , :
98	instantiation	244, 231, 111	,  ⊢
	: , : , :
99	instantiation	115, 116, 123, 112	,  ⊢
	: , :
100	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
101	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
102	instantiation	244, 231, 113	,  ⊢
	: , : , :
103	instantiation	210, 114	⊢
	:
104	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
105	instantiation	115, 116, 145, 117	,  ⊢
	: , :
106	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
107	instantiation	218, 219, 236	⊢
	: , : , :
108	instantiation	118, 236	⊢
	:
109	instantiation	192, 208, 119	⊢
	: , :
110	instantiation	133, 120, 121	⊢
	: , : , :
111	instantiation	244, 239, 123	,  ⊢
	: , : , :
112	instantiation	122, 123, 124, 125	,  ⊢
	: , :
113	instantiation	244, 239, 145	,  ⊢
	: , : , :
114	instantiation	126, 166, 127	⊢
	: , :
115	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_not_eq_nonzeroInt
116	instantiation	128, 129, 246, 130	⊢
	: , : , : , : , :
117	instantiation	211, 131	,  ⊢
	:
118	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
119	instantiation	244, 221, 132	⊢
	: , : , :
120	instantiation	133, 134, 135	⊢
	: , : , :
121	instantiation	136, 137, 138	⊢
	: , :
122	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_int
123	instantiation	244, 139, 156	,  ⊢
	: , : , :
124	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
125	instantiation	140, 141, 142	,  ⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
127	instantiation	143, 144	⊢
	:
128	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
129	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
130	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
131	instantiation	189, 145, 146	,  ⊢
	:
132	instantiation	244, 231, 147	⊢
	: , : , :
133	axiom		⊢
	proveit.logic.equality.equals_transitivity
134	instantiation	186, 162	⊢
	: , : , :
135	instantiation	186, 148	⊢
	: , : , :
136	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
137	instantiation	149, 150, 151	⊢
	: , :
138	instantiation	152	⊢
	:
139	instantiation	214, 154, 155	⊢
	: , :
140	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
141	instantiation	153, 154, 155, 156	,  ⊢
	: , : , :
142	instantiation	157, 158	⊢
	:
143	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
144	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
145	instantiation	244, 159, 172	,  ⊢
	: , : , :
146	instantiation	203, 160, 161	,  ⊢
	: , : , :
147	instantiation	244, 239, 167	⊢
	: , : , :
148	instantiation	186, 162	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
150	instantiation	163, 208, 164, 165	⊢
	: , :
151	instantiation	244, 221, 166	⊢
	: , : , :
152	axiom		⊢
	proveit.logic.equality.equals_reflexivity
153	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
154	instantiation	226, 167, 240	⊢
	: , :
155	instantiation	237, 171	⊢
	:
156	assumption		⊢
157	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
158	instantiation	168, 170	⊢
	:
159	instantiation	214, 171, 227	⊢
	: , :
160	instantiation	169, 170	⊢
	:
161	instantiation	215, 171, 227, 172	,  ⊢
	: , : , :
162	instantiation	173, 174, 175, 176	⊢
	: , : , : , :
163	theorem		⊢
	proveit.numbers.division.div_complex_closure
164	instantiation	177, 196, 208	⊢
	: , :
165	instantiation	178, 198, 179	⊢
	: , : , :
166	instantiation	218, 219, 180	⊢
	: , : , :
167	instantiation	237, 227	⊢
	:
168	theorem		⊢
	proveit.numbers.negation.int_neg_closure
169	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
170	instantiation	181, 182, 201	⊢
	: , :
171	instantiation	226, 190, 240	⊢
	: , :
172	assumption		⊢
173	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
174	instantiation	186, 183	⊢
	: , : , :
175	instantiation	184, 185	⊢
	: , :
176	instantiation	186, 187	⊢
	: , : , :
177	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
178	theorem		⊢
	proveit.logic.equality.sub_left_side_into
179	instantiation	188, 196	⊢
	:
180	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
181	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
182	instantiation	189, 190, 191	⊢
	:
183	instantiation	192, 193, 194	⊢
	: , :
184	theorem		⊢
	proveit.logic.equality.equals_reversal
185	instantiation	195, 196, 197, 206, 198	⊢
	: , : , :
186	axiom		⊢
	proveit.logic.equality.substitution
187	instantiation	199, 200, 201	⊢
	: , :
188	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
189	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
190	instantiation	244, 202, 217	⊢
	: , : , :
191	instantiation	203, 204, 205	⊢
	: , : , :
192	theorem		⊢
	proveit.numbers.addition.commutation
193	instantiation	244, 221, 206	⊢
	: , : , :
194	instantiation	207, 208	⊢
	:
195	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
196	instantiation	244, 221, 209	⊢
	: , : , :
197	instantiation	210, 222	⊢
	:
198	instantiation	211, 242	⊢
	:
199	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
200	instantiation	244, 212, 213	⊢
	: , : , :
201	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
202	instantiation	214, 240, 216	⊢
	: , :
203	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
204	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
205	instantiation	215, 240, 216, 217	⊢
	: , : , :
206	instantiation	218, 219, 220	⊢
	: , : , :
207	theorem		⊢
	proveit.numbers.negation.complex_closure
208	instantiation	244, 221, 222	⊢
	: , : , :
209	instantiation	244, 231, 223	⊢
	: , : , :
210	theorem		⊢
	proveit.numbers.negation.real_closure
211	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
212	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
213	instantiation	244, 224, 225	⊢
	: , : , :
214	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
215	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
216	instantiation	226, 227, 228	⊢
	: , :
217	assumption		⊢
218	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
219	instantiation	229, 230	⊢
	: , :
220	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
221	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
222	instantiation	244, 231, 232	⊢
	: , : , :
223	instantiation	244, 239, 238	⊢
	: , : , :
224	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
225	instantiation	244, 233, 234	⊢
	: , : , :
226	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
227	instantiation	244, 235, 236	⊢
	: , : , :
228	instantiation	237, 238	⊢
	:
229	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
230	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
231	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
232	instantiation	244, 239, 240	⊢
	: , : , :
233	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
234	instantiation	244, 241, 242	⊢
	: , : , :
235	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
236	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
237	theorem		⊢
	proveit.numbers.negation.int_closure
238	instantiation	244, 245, 243	⊢
	: , : , :
239	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
240	instantiation	244, 245, 246	⊢
	: , : , :
241	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
242	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
243	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
244	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
245	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
246	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements