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