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