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