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	26	⊢
2	instantiation	4, 404	⊢
	:
3	instantiation	359, 5, 6, 7*	⊢
	: , : , :
4	theorem		⊢
	proveit.physics.quantum.QPE._failure_upper_bound_lemma
5	instantiation	359, 8, 9	⊢
	: , : , :
6	instantiation	10, 387, 369, 11	⊢
	: , : , : , :
7	instantiation	294, 12, 13	⊢
	: , : , :
8	instantiation	359, 14, 15	⊢
	: , : , :
9	instantiation	16, 341, 342, 17*, 18*, 19*	⊢
	: , : , : , :
10	theorem		⊢
	proveit.numbers.summation.sum_split_first
11	instantiation	359, 20, 21	⊢
	: , : , :
12	instantiation	145, 22	⊢
	: , : , :
13	instantiation	151, 405, 415, 334, 23, 335, 72, 24, 95, 25*	⊢
	: , : , : , : , : , :
14	instantiation	26, 27, 28	⊢
	: , : , :
15	instantiation	29, 368, 407, 381, 30*, 31*	⊢
	: , : , : , : , :
16	theorem		⊢
	proveit.numbers.summation.index_negate
17	instantiation	179, 32	⊢
	:
18	instantiation	33, 34, 373, 35*	⊢
	: , :
19	instantiation	36, 37, 405, 165*	,  ⊢
	: , :
20	instantiation	38, 346, 39, 383, 40, 395	⊢
	: , : , :
21	instantiation	294, 41, 42	⊢
	: , : , :
22	instantiation	294, 43, 44	⊢
	: , : , :
23	instantiation	349	⊢
	: , :
24	instantiation	45, 351, 183	⊢
	: , :
25	instantiation	294, 46, 47	⊢
	: , : , :
26	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
27	instantiation	50, 97, 48, 51, 49, 54	⊢
	: , : , :
28	instantiation	50, 97, 51, 52, 53, 54	⊢
	: , : , :
29	theorem		⊢
	proveit.numbers.summation.index_shift
30	instantiation	294, 55, 56	⊢
	: , : , :
31	instantiation	294, 57, 58	,  ⊢
	: , : , :
32	instantiation	413, 382, 59	⊢
	: , : , :
33	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
34	instantiation	413, 382, 60	⊢
	: , : , :
35	instantiation	179, 64	⊢
	:
36	theorem		⊢
	proveit.numbers.exponentiation.even_pow_is_even_fn
37	instantiation	413, 382, 279	,  ⊢
	: , : , :
38	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
39	instantiation	413, 391, 61	⊢
	: , : , :
40	instantiation	321, 402, 403, 404	⊢
	: , : , :
41	instantiation	121, 334, 415, 405, 335, 62, 64, 127, 373	⊢
	: , : , : , : , : , :
42	instantiation	93, 405, 415, 334, 63, 335, 64, 127, 373, 65*	⊢
	: , : , : , : , : , :
43	instantiation	121, 405, 415, 334, 66, 335, 183, 95	⊢
	: , : , : , : , : , :
44	instantiation	294, 67, 68	⊢
	: , : , :
45	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
46	instantiation	314, 405, 415, 334, 69, 335, 72, 351, 183	⊢
	: , : , : , : , : , :
47	instantiation	70, 334, 415, 405, 335, 71, 72, 351, 183, 73*	⊢
	: , : , : , : , : , :
48	instantiation	286, 75, 78	⊢
	: , :
49	instantiation	74, 78, 75, 77, 76	⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
51	instantiation	286, 77, 78	⊢
	: , :
52	instantiation	286, 77, 79	⊢
	: , :
53	instantiation	232, 77, 78, 79, 80	⊢
	: , : , :
54	instantiation	290, 81	⊢
	: , :
55	instantiation	121, 334, 415, 405, 335, 82, 83, 373, 315	⊢
	: , : , : , : , : , :
56	instantiation	123, 373, 83, 125	⊢
	: , : , :
57	instantiation	145, 84	⊢
	: , : , :
58	instantiation	294, 85, 86	,  ⊢
	: , : , :
59	instantiation	413, 391, 87	⊢
	: , : , :
60	instantiation	413, 391, 88	⊢
	: , : , :
61	instantiation	413, 399, 403	⊢
	: , : , :
62	instantiation	349	⊢
	: , :
63	instantiation	349	⊢
	: , :
64	instantiation	413, 382, 89	⊢
	: , : , :
65	instantiation	359, 90, 91	⊢
	: , : , :
66	instantiation	349	⊢
	: , :
67	instantiation	92, 405, 334, 335, 183, 95	⊢
	: , : , : , : , : , : , :
68	instantiation	93, 334, 415, 405, 335, 94, 183, 95, 96*	⊢
	: , : , : , : , : , :
69	instantiation	349	⊢
	: , :
70	theorem		⊢
	proveit.numbers.multiplication.association
71	instantiation	349	⊢
	: , :
72	instantiation	413, 382, 97	⊢
	: , : , :
73	instantiation	98, 373, 351, 99, 100, 101*, 102*	⊢
	: , : , : , :
74	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
75	modus ponens	103, 104	⊢
76	modus ponens	105, 106	⊢
77	modus ponens	107, 108	⊢
78	modus ponens	109, 110	⊢
79	modus ponens	111, 112	⊢
80	modus ponens	113, 114	⊢
81	instantiation	115, 155	⊢
	:
82	instantiation	349	⊢
	: , :
83	instantiation	413, 382, 346	⊢
	: , : , :
84	instantiation	116, 320, 117, 118, 119, 120	⊢
	: , : , :
85	instantiation	121, 334, 415, 405, 335, 122, 124, 373, 315	,  ⊢
	: , : , : , : , : , :
86	instantiation	123, 373, 124, 125	,  ⊢
	: , : , :
87	instantiation	413, 399, 368	⊢
	: , : , :
88	instantiation	413, 399, 357	⊢
	: , : , :
89	instantiation	376, 377, 410	⊢
	: , : , :
90	instantiation	126, 373, 351, 131	⊢
	: , : , :
91	instantiation	372, 373, 127	⊢
	: , :
92	theorem		⊢
	proveit.numbers.addition.leftward_commutation
93	theorem		⊢
	proveit.numbers.addition.association
94	instantiation	349	⊢
	: , :
95	instantiation	413, 382, 128	⊢
	: , : , :
96	instantiation	129, 130, 131*	⊢
	: , :
97	instantiation	413, 391, 132	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.division.prod_of_fracs
99	instantiation	413, 190, 133	⊢
	: , : , :
100	instantiation	413, 190, 134	⊢
	: , : , :
101	instantiation	135, 351	⊢
	:
102	instantiation	294, 136, 137	⊢
	: , : , :
103	instantiation	242	⊢
	: , : , :
104	generalization	138	⊢
105	instantiation	143	⊢
	: , : , :
106	generalization	139	⊢
107	instantiation	242	⊢
	: , : , :
108	generalization	140	⊢
109	instantiation	242	⊢
	: , : , :
110	generalization	141	⊢
111	instantiation	242	⊢
	: , : , :
112	generalization	142	⊢
113	instantiation	143	⊢
	: , : , :
114	generalization	144	⊢
115	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
116	theorem		⊢
	proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
117	instantiation	349	⊢
	: , :
118	instantiation	349	⊢
	: , :
119	instantiation	145, 146	⊢
	: , : , :
120	instantiation	215	⊢
	:
121	theorem		⊢
	proveit.numbers.addition.disassociation
122	instantiation	349	⊢
	: , :
123	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
124	instantiation	413, 382, 147	,  ⊢
	: , : , :
125	instantiation	215	⊢
	:
126	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
127	instantiation	413, 382, 148	⊢
	: , : , :
128	instantiation	259, 383, 149, 150	⊢
	: , :
129	theorem		⊢
	proveit.logic.equality.equals_reversal
130	instantiation	151, 334, 415, 405, 335, 152, 373, 183, 153*	⊢
	: , : , : , : , : , :
131	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
132	instantiation	413, 154, 155	⊢
	: , : , :
133	instantiation	413, 211, 156	⊢
	: , : , :
134	instantiation	413, 211, 157	⊢
	: , : , :
135	theorem		⊢
	proveit.numbers.division.frac_one_denom
136	instantiation	158, 415, 159, 160, 161, 162	⊢
	: , : , : , :
137	instantiation	163, 164, 373, 165*, 166*	⊢
	: , : , :
138	instantiation	259, 383, 167, 168	,  ⊢
	: , :
139	instantiation	169, 170, 216, 212, 171	,  ⊢
	: , : , :
140	instantiation	259, 383, 172, 173	,  ⊢
	: , :
141	instantiation	259, 383, 174, 175	,  ⊢
	: , :
142	instantiation	259, 383, 176, 177	,  ⊢
	: , :
143	theorem		⊢
	proveit.numbers.summation.weak_summation_from_summands_bound
144	instantiation	290, 178	,  ⊢
	: , :
145	axiom		⊢
	proveit.logic.equality.substitution
146	instantiation	179, 373	⊢
	:
147	instantiation	413, 391, 180	,  ⊢
	: , : , :
148	instantiation	413, 391, 181	⊢
	: , : , :
149	instantiation	278, 346, 415	⊢
	: , :
150	instantiation	280, 182, 282	⊢
	: , :
151	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
152	instantiation	349	⊢
	: , :
153	instantiation	188, 183	⊢
	:
154	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
155	instantiation	184, 219, 185	⊢
	: , :
156	instantiation	413, 299, 186	⊢
	: , : , :
157	instantiation	413, 299, 187	⊢
	: , : , :
158	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
159	instantiation	349	⊢
	: , :
160	instantiation	349	⊢
	: , :
161	instantiation	188, 351	⊢
	:
162	instantiation	313, 189	⊢
	:
163	theorem		⊢
	proveit.numbers.division.frac_cancel_left
164	instantiation	413, 190, 191	⊢
	: , : , :
165	instantiation	313, 351	⊢
	:
166	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
167	instantiation	278, 245, 415	,  ⊢
	: , :
168	instantiation	199, 192	,  ⊢
	:
169	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
170	instantiation	413, 193, 194	⊢
	: , : , :
171	instantiation	195, 362, 245, 266, 196, 197	,  ⊢
	: , : , :
172	instantiation	278, 266, 415	,  ⊢
	: , :
173	instantiation	199, 198	,  ⊢
	:
174	instantiation	278, 268, 415	,  ⊢
	: , :
175	instantiation	199, 200	,  ⊢
	:
176	instantiation	278, 223, 415	,  ⊢
	: , :
177	instantiation	201, 239	,  ⊢
	:
178	instantiation	202, 203, 204, 218, 205	,  ⊢
	: , : , :
179	theorem		⊢
	proveit.numbers.negation.double_negation
180	instantiation	413, 399, 206	,  ⊢
	: , : , :
181	instantiation	413, 399, 408	⊢
	: , : , :
182	instantiation	413, 299, 207	⊢
	: , : , :
183	instantiation	413, 382, 208	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
185	instantiation	413, 238, 209	⊢
	: , : , :
186	instantiation	413, 319, 209	⊢
	: , : , :
187	instantiation	413, 319, 398	⊢
	: , : , :
188	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
189	instantiation	413, 382, 210	⊢
	: , : , :
190	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
191	instantiation	413, 211, 282	⊢
	: , : , :
192	instantiation	413, 217, 212	,  ⊢
	: , : , :
193	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
194	instantiation	413, 213, 405	⊢
	: , : , :
195	theorem		⊢
	proveit.numbers.exponentiation.exp_even_neg_base_lesseq
196	instantiation	240, 214, 283	,  ⊢
	: , :
197	instantiation	215	⊢
	:
198	instantiation	413, 217, 216	,  ⊢
	: , : , :
199	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
200	instantiation	413, 217, 218	,  ⊢
	: , : , :
201	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
202	theorem		⊢
	proveit.numbers.division.strong_div_from_denom_bound__all_pos
203	instantiation	413, 220, 219	⊢
	: , : , :
204	instantiation	413, 220, 221	,  ⊢
	: , : , :
205	instantiation	222, 362, 223, 268, 224, 225	,  ⊢
	: , : , :
206	instantiation	413, 226, 227	,  ⊢
	: , : , :
207	instantiation	413, 319, 380	⊢
	: , : , :
208	modus ponens	228, 229	⊢
209	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
210	instantiation	413, 391, 230	⊢
	: , : , :
211	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
212	instantiation	236, 245, 231	,  ⊢
	:
213	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
214	instantiation	232, 266, 288, 345, 233, 234*	,  ⊢
	: , : , :
215	axiom		⊢
	proveit.logic.equality.equals_reflexivity
216	instantiation	236, 266, 235	,  ⊢
	:
217	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
218	instantiation	236, 268, 237	,  ⊢
	:
219	instantiation	413, 238, 398	⊢
	: , : , :
220	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
221	instantiation	413, 238, 239	,  ⊢
	: , : , :
222	theorem		⊢
	proveit.numbers.exponentiation.exp_pos_less
223	instantiation	286, 287, 274	,  ⊢
	: , :
224	instantiation	240, 272, 241	,  ⊢
	: , :
225	instantiation	366, 320	⊢
	:
226	instantiation	400, 387, 369	⊢
	: , :
227	assumption		⊢
228	instantiation	242	⊢
	: , : , :
229	generalization	243	⊢
230	instantiation	413, 399, 244	⊢
	: , : , :
231	instantiation	267, 245, 345, 246	,  ⊢
	: , :
232	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
233	instantiation	247, 274, 345, 308, 284, 248, 277*, 249*	⊢
	: , : , :
234	instantiation	371, 250	,  ⊢
	:
235	instantiation	251, 305, 252, 283	,  ⊢
	: , :
236	theorem		⊢
	proveit.numbers.exponentiation.sqrd_pos_closure
237	instantiation	253, 254	,  ⊢
	: , :
238	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
239	instantiation	255, 256, 415	,  ⊢
	: , :
240	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
241	instantiation	257, 287, 274, 288, 258	,  ⊢
	: , : , :
242	theorem		⊢
	proveit.numbers.summation.summation_real_closure
243	instantiation	259, 383, 260, 261	,  ⊢
	: , :
244	instantiation	413, 414, 262	⊢
	: , : , :
245	instantiation	286, 266, 288	,  ⊢
	: , :
246	instantiation	263, 264	,  ⊢
	: , :
247	theorem		⊢
	proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
248	instantiation	290, 275	⊢
	: , :
249	instantiation	265, 315	⊢
	:
250	instantiation	413, 382, 266	,  ⊢
	: , : , :
251	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_int
252	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
253	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
254	instantiation	267, 345, 268, 269	,  ⊢
	: , :
255	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
256	instantiation	270, 271, 272	,  ⊢
	:
257	theorem		⊢
	proveit.numbers.addition.strong_bound_via_right_term_bound
258	instantiation	273, 274, 308, 383, 310, 275, 276*, 277*	⊢
	: , : , :
259	theorem		⊢
	proveit.numbers.division.div_real_closure
260	instantiation	278, 279, 415	,  ⊢
	: , :
261	instantiation	280, 281, 282	,  ⊢
	: , :
262	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
263	theorem		⊢
	proveit.numbers.addition.subtraction.neg_difference
264	instantiation	394, 283, 284	,  ⊢
	: , : , :
265	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
266	instantiation	413, 391, 285	,  ⊢
	: , : , :
267	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq
268	instantiation	286, 287, 288	,  ⊢
	: , :
269	instantiation	311, 289	,  ⊢
	: , :
270	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
271	instantiation	406, 326, 381	,  ⊢
	: , :
272	instantiation	290, 291	,  ⊢
	: , :
273	theorem		⊢
	proveit.numbers.multiplication.reversed_strong_bound_via_right_factor_bound
274	instantiation	307, 383	⊢
	:
275	instantiation	322, 390	⊢
	:
276	instantiation	292, 373, 293*	⊢
	: , :
277	instantiation	294, 295, 296	⊢
	: , : , :
278	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
279	instantiation	413, 391, 297	,  ⊢
	: , : , :
280	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
281	instantiation	413, 299, 298	,  ⊢
	: , : , :
282	instantiation	413, 299, 300	⊢
	: , : , :
283	instantiation	301, 302, 303	,  ⊢
	: , : , :
284	instantiation	304, 345, 383, 329	⊢
	: , : , :
285	instantiation	413, 399, 305	,  ⊢
	: , : , :
286	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
287	instantiation	413, 391, 306	,  ⊢
	: , : , :
288	instantiation	307, 308	⊢
	:
289	instantiation	309, 310, 312	,  ⊢
	: , : , :
290	theorem		⊢
	proveit.numbers.ordering.relax_less
291	instantiation	311, 312	,  ⊢
	: , :
292	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
293	instantiation	313, 373	⊢
	:
294	axiom		⊢
	proveit.logic.equality.equals_transitivity
295	instantiation	314, 405, 415, 334, 336, 335, 315, 337, 338	⊢
	: , : , : , : , : , :
296	instantiation	316, 334, 415, 335, 336, 373, 337, 338, 317*	⊢
	: , : , : , : , :
297	instantiation	413, 399, 339	,  ⊢
	: , : , :
298	instantiation	413, 319, 318	,  ⊢
	: , : , :
299	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
300	instantiation	413, 319, 320	⊢
	: , : , :
301	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
302	instantiation	321, 341, 342, 325	,  ⊢
	: , : , :
303	instantiation	322, 323	⊢
	:
304	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
305	instantiation	413, 324, 325	,  ⊢
	: , : , :
306	instantiation	413, 399, 326	,  ⊢
	: , : , :
307	theorem		⊢
	proveit.numbers.negation.real_closure
308	instantiation	327, 345, 383, 329	⊢
	: , : , :
309	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
310	instantiation	328, 345, 383, 329	⊢
	: , : , :
311	theorem		⊢
	proveit.numbers.addition.subtraction.pos_difference
312	instantiation	394, 330, 331	,  ⊢
	: , : , :
313	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
314	theorem		⊢
	proveit.numbers.multiplication.disassociation
315	instantiation	332, 373	⊢
	:
316	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
317	instantiation	333, 334, 415, 335, 336, 337, 338	⊢
	: , : , : , :
318	instantiation	386, 339, 340	,  ⊢
	:
319	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
320	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
321	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
322	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
323	instantiation	397, 367	⊢
	:
324	instantiation	400, 341, 342	⊢
	: , :
325	assumption		⊢
326	instantiation	413, 343, 348	,  ⊢
	: , : , :
327	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
328	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
329	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
330	instantiation	344, 383, 345, 346, 388, 347*	⊢
	: , : , :
331	instantiation	401, 368, 407, 348	,  ⊢
	: , : , :
332	theorem		⊢
	proveit.numbers.negation.complex_closure
333	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
334	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
335	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
336	instantiation	349	⊢
	: , :
337	instantiation	350, 351, 352	⊢
	: , :
338	instantiation	413, 382, 353	⊢
	: , : , :
339	instantiation	413, 354, 370	,  ⊢
	: , : , :
340	instantiation	394, 355, 356	,  ⊢
	: , : , :
341	instantiation	406, 357, 402	⊢
	: , :
342	instantiation	411, 368	⊢
	:
343	instantiation	400, 368, 407	⊢
	: , :
344	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
345	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
346	instantiation	413, 391, 358	⊢
	: , : , :
347	instantiation	359, 360, 361	⊢
	: , : , :
348	assumption		⊢
349	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
350	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
351	instantiation	413, 382, 362	⊢
	: , : , :
352	instantiation	413, 382, 363	⊢
	: , : , :
353	instantiation	364, 365	⊢
	:
354	instantiation	400, 368, 369	⊢
	: , :
355	instantiation	366, 367	⊢
	:
356	instantiation	401, 368, 369, 370	,  ⊢
	: , : , :
357	instantiation	411, 407	⊢
	:
358	instantiation	413, 399, 387	⊢
	: , : , :
359	theorem		⊢
	proveit.logic.equality.sub_right_side_into
360	instantiation	371, 373	⊢
	:
361	instantiation	372, 373, 374	⊢
	: , :
362	instantiation	413, 391, 375	⊢
	: , : , :
363	instantiation	376, 377, 378	⊢
	: , : , :
364	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
365	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
366	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
367	instantiation	379, 380, 398	⊢
	: , :
368	instantiation	406, 387, 402	⊢
	: , :
369	instantiation	406, 407, 381	⊢
	: , :
370	assumption		⊢
371	theorem		⊢
	proveit.numbers.addition.elim_zero_right
372	theorem		⊢
	proveit.numbers.addition.commutation
373	instantiation	413, 382, 383	⊢
	: , : , :
374	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
375	instantiation	413, 399, 412	⊢
	: , : , :
376	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
377	instantiation	384, 385	⊢
	: , :
378	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
379	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
380	instantiation	386, 387, 388	⊢
	:
381	instantiation	413, 389, 390	⊢
	: , : , :
382	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
383	instantiation	413, 391, 392	⊢
	: , : , :
384	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
385	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
386	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
387	instantiation	413, 393, 404	⊢
	: , : , :
388	instantiation	394, 395, 396	⊢
	: , : , :
389	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
390	instantiation	397, 398	⊢
	:
391	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
392	instantiation	413, 399, 402	⊢
	: , : , :
393	instantiation	400, 402, 403	⊢
	: , :
394	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
395	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
396	instantiation	401, 402, 403, 404	⊢
	: , : , :
397	theorem		⊢
	proveit.numbers.negation.int_neg_closure
398	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
399	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
400	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
401	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
402	instantiation	413, 414, 405	⊢
	: , : , :
403	instantiation	406, 407, 408	⊢
	: , :
404	assumption		⊢
405	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
406	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
407	instantiation	413, 409, 410	⊢
	: , : , :
408	instantiation	411, 412	⊢
	:
409	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
410	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
411	theorem		⊢
	proveit.numbers.negation.int_closure
412	instantiation	413, 414, 415	⊢
	: , : , :
413	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
414	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
415	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements