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	305	⊢
2	instantiation	4, 5	⊢
	:
3	instantiation	531, 6, 7	,  ⊢
	: , : , :
4	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
5	instantiation	416, 36	⊢
	:
6	instantiation	531, 8, 9	,  ⊢
	: , : , :
7	instantiation	10, 655, 657, 548, 549, 60, 11, 499, 12, 13*	,  ⊢
	: , : , : , : , : , :
8	instantiation	292, 14, 15	,  ⊢
	: , : , :
9	instantiation	490, 655, 657, 548, 156, 549, 630, 426, 343	⊢
	: , : , : , : , : , :
10	theorem		⊢
	proveit.numbers.multiplication.distribute_through_abs_sum
11	instantiation	604	⊢
	: , :
12	instantiation	658, 636, 16	,  ⊢
	: , : , :
13	instantiation	496, 426, 17, 18*	,  ⊢
	: , :
14	instantiation	19, 20, 21	,  ⊢
	: , : , :
15	instantiation	531, 22, 23	,  ⊢
	: , : , :
16	instantiation	658, 643, 24	,  ⊢
	: , : , :
17	instantiation	658, 636, 25	,  ⊢
	: , : , :
18	instantiation	531, 26, 27	⊢
	: , : , :
19	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
20	instantiation	28, 56, 109, 637, 29, 57	,  ⊢
	: , : , :
21	instantiation	30, 59, 31, 32, 33, 34*	,  ⊢
	: , : , :
22	instantiation	35, 36, 37, 38, 39*	,  ⊢
	: , :
23	instantiation	251, 600, 75, 195, 40, 41*, 42*	,  ⊢
	: , : , : , :
24	instantiation	658, 625, 43	,  ⊢
	: , : , :
25	instantiation	658, 643, 44	,  ⊢
	: , : , :
26	instantiation	531, 45, 46	⊢
	: , : , :
27	instantiation	534, 47, 48, 49	⊢
	: , : , : , :
28	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
29	instantiation	50, 600, 209, 51*	⊢
	: , :
30	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
31	instantiation	52, 485, 53, 54, 90, 372	,  ⊢
	: , :
32	instantiation	55, 56, 57	,  ⊢
	:
33	instantiation	58, 657, 548, 226, 549, 59, 60, 122, 61*	,  ⊢
	: , : , : , : , : , :
34	instantiation	534, 62, 63, 64	,  ⊢
	: , : , : , :
35	theorem		⊢
	proveit.numbers.absolute_value.abs_eq
36	instantiation	65, 66	⊢
	:
37	instantiation	484, 69, 70	,  ⊢
	: , :
38	instantiation	67, 632, 461	,  ⊢
	:
39	instantiation	298, 649, 68, 69, 70, 71*, 72*	,  ⊢
	: , :
40	instantiation	73, 567, 74	,  ⊢
	: , :
41	instantiation	620, 75	⊢
	:
42	instantiation	609, 76, 77	,  ⊢
	: , : , :
43	instantiation	78, 79	,  ⊢
	:
44	instantiation	658, 625, 79	,  ⊢
	: , : , :
45	instantiation	80, 600, 551, 195, 566	⊢
	: , : , : , : , :
46	instantiation	609, 81, 82	⊢
	: , : , :
47	instantiation	621, 570	⊢
	: , : , :
48	instantiation	621, 83	⊢
	: , : , :
49	instantiation	620, 551	⊢
	:
50	theorem		⊢
	proveit.numbers.absolute_value.triangle_inequality
51	instantiation	609, 84, 85	⊢
	: , : , :
52	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure
53	instantiation	506	⊢
	: , : , :
54	instantiation	658, 213, 86	⊢
	: , : , :
55	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
56	instantiation	531, 87, 88	,  ⊢
	: , : , :
57	instantiation	89, 657, 548, 226, 549, 183, 90, 91, 92*	,  ⊢
	: , : , : , : , : , :
58	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_factor_bound
59	instantiation	658, 94, 93	⊢
	: , : , :
60	instantiation	658, 94, 95	⊢
	: , : , :
61	instantiation	609, 96, 97	⊢
	: , : , :
62	instantiation	609, 98, 99	,  ⊢
	: , : , :
63	instantiation	615	⊢
	:
64	instantiation	411, 100	,  ⊢
	: , :
65	theorem		⊢
	proveit.physics.quantum.QPE._alpha_are_complex
66	instantiation	101, 575, 624	⊢
	: , :
67	theorem		⊢
	proveit.physics.quantum.QPE._alpha_summed
68	instantiation	604	⊢
	: , :
69	instantiation	658, 636, 102	⊢
	: , : , :
70	instantiation	250, 177, 105, 106	,  ⊢
	: , :
71	instantiation	331, 103	⊢
	:
72	instantiation	104, 177, 105, 106, 107*	,  ⊢
	: , :
73	theorem		⊢
	proveit.numbers.multiplication.mult_complex_nonzero_closure_bin
74	instantiation	417, 119, 108	,  ⊢
	:
75	instantiation	658, 636, 109	⊢
	: , : , :
76	instantiation	546, 655, 657, 548, 110, 549, 426, 630, 119	,  ⊢
	: , : , : , : , : , :
77	instantiation	489, 548, 655, 549, 426, 630, 119	,  ⊢
	: , : , : , : , : , : , :
78	theorem		⊢
	proveit.numbers.negation.rational_nonzero_closure
79	instantiation	111, 112, 255	,  ⊢
	: , :
80	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
81	instantiation	621, 113	⊢
	: , : , :
82	instantiation	621, 114	⊢
	: , : , :
83	instantiation	623, 551	⊢
	:
84	instantiation	586, 657, 115, 116, 117, 118	⊢
	: , : , : , :
85	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
86	instantiation	658, 585, 564	⊢
	: , : , :
87	instantiation	596, 254, 175	,  ⊢
	: , :
88	instantiation	546, 548, 657, 655, 549, 226, 630, 426, 119	,  ⊢
	: , : , : , : , : , :
89	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
90	instantiation	658, 213, 198	⊢
	: , : , :
91	instantiation	120, 121, 122	,  ⊢
	: , : , :
92	instantiation	123, 657, 548, 226, 549, 630, 426	⊢
	: , : , : , :
93	instantiation	658, 124, 657	⊢
	: , : , :
94	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
95	instantiation	658, 124, 125	⊢
	: , : , :
96	instantiation	546, 657, 548, 226, 342, 549, 630, 426, 343	⊢
	: , : , : , : , : , :
97	instantiation	609, 126, 127	⊢
	: , : , :
98	instantiation	621, 128	⊢
	: , : , :
99	instantiation	477, 630, 129, 130, 131*	,  ⊢
	: , :
100	instantiation	609, 132, 133	,  ⊢
	: , : , :
101	theorem		⊢
	proveit.physics.quantum.QPE._mod_add_closure
102	instantiation	658, 643, 134	⊢
	: , : , :
103	instantiation	359, 135	⊢
	: , :
104	theorem		⊢
	proveit.numbers.absolute_value.abs_frac
105	instantiation	399, 600, 136	⊢
	: , :
106	instantiation	441, 137	,  ⊢
	: , :
107	instantiation	138, 438, 139, 140*, 141*, 142*	,  ⊢
	: , :
108	instantiation	233, 143	,  ⊢
	: , :
109	instantiation	658, 395, 144	⊢
	: , : , :
110	instantiation	604	⊢
	: , :
111	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
112	instantiation	145, 612, 461	,  ⊢
	:
113	instantiation	609, 146, 147	⊢
	: , : , :
114	instantiation	621, 148	⊢
	: , : , :
115	instantiation	604	⊢
	: , :
116	instantiation	604	⊢
	: , :
117	instantiation	331, 149	⊢
	:
118	instantiation	271, 245, 150*	⊢
	:
119	instantiation	658, 636, 175	,  ⊢
	: , : , :
120	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
121	instantiation	407, 151	,  ⊢
	:
122	instantiation	152, 153, 336, 154*	,  ⊢
	:
123	theorem		⊢
	proveit.numbers.multiplication.mult_zero_any
124	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
125	instantiation	658, 155, 474	⊢
	: , : , :
126	instantiation	489, 655, 630, 426, 343	⊢
	: , : , : , : , : , : , :
127	instantiation	490, 548, 657, 549, 588, 156, 630, 426, 343, 527*	⊢
	: , : , : , : , : , :
128	instantiation	621, 321	⊢
	: , : , :
129	instantiation	531, 157, 158	⊢
	: , : , :
130	instantiation	376, 485, 218, 252, 195, 289	,  ⊢
	: , :
131	instantiation	609, 159, 160	,  ⊢
	: , : , :
132	instantiation	621, 161	⊢
	: , : , :
133	instantiation	477, 600, 162, 163, 164*	,  ⊢
	: , :
134	instantiation	658, 522, 165	⊢
	: , : , :
135	instantiation	408, 165	⊢
	:
136	instantiation	495, 166	⊢
	:
137	instantiation	292, 167, 168	,  ⊢
	: , : , :
138	theorem		⊢
	proveit.trigonometry.complex_unit_circle_chord_length
139	instantiation	531, 384, 357	⊢
	: , : , :
140	instantiation	609, 169, 170	⊢
	: , : , :
141	instantiation	411, 171	⊢
	: , :
142	instantiation	609, 172, 173	,  ⊢
	: , : , :
143	instantiation	174, 438, 175, 176	,  ⊢
	: , :
144	instantiation	416, 177	⊢
	:
145	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
146	instantiation	621, 178	⊢
	: , : , :
147	instantiation	623, 426	⊢
	:
148	instantiation	629, 426	⊢
	:
149	instantiation	358, 655	⊢
	:
150	instantiation	179, 180, 181*	⊢
	:
151	instantiation	182, 183, 372	,  ⊢
	: , :
152	theorem		⊢
	proveit.trigonometry.sine_linear_bound_nonneg
153	instantiation	184, 304, 185	,  ⊢
	:
154	instantiation	609, 186, 187	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
156	instantiation	604	⊢
	: , :
157	instantiation	484, 188, 290	⊢
	: , :
158	instantiation	546, 548, 657, 655, 549, 189, 529, 426, 290	⊢
	: , : , : , : , : , :
159	instantiation	621, 190	,  ⊢
	: , : , :
160	instantiation	609, 191, 192	⊢
	: , : , :
161	instantiation	621, 321	⊢
	: , : , :
162	instantiation	531, 193, 194	⊢
	: , : , :
163	instantiation	376, 485, 257, 567, 195, 289	,  ⊢
	: , :
164	instantiation	609, 196, 197	,  ⊢
	: , : , :
165	instantiation	558, 559, 198	⊢
	: , :
166	instantiation	509, 277, 199	⊢
	: , :
167	instantiation	292, 200, 201	,  ⊢
	: , : , :
168	instantiation	621, 202	⊢
	: , : , :
169	instantiation	621, 203	⊢
	: , : , :
170	instantiation	578, 277	⊢
	:
171	instantiation	621, 204	⊢
	: , : , :
172	instantiation	621, 205	⊢
	: , : , :
173	instantiation	609, 206, 207	,  ⊢
	: , : , :
174	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq
175	instantiation	333, 438, 614, 208	,  ⊢
	: , : , :
176	instantiation	334, 438, 614, 208	,  ⊢
	: , : , :
177	instantiation	399, 600, 209	⊢
	: , :
178	instantiation	620, 426	⊢
	:
179	theorem		⊢
	proveit.numbers.absolute_value.complex_unit_length
180	instantiation	531, 210, 211	⊢
	: , : , :
181	instantiation	411, 212	⊢
	: , :
182	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
183	instantiation	658, 213, 560	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_real_is_real_nonneg
185	instantiation	359, 306	,  ⊢
	: , :
186	instantiation	621, 214	⊢
	: , : , :
187	instantiation	609, 215, 216	⊢
	: , : , :
188	instantiation	658, 636, 217	⊢
	: , : , :
189	instantiation	604	⊢
	: , :
190	instantiation	256, 299, 218, 529, 426, 290, 538, 530, 427, 258, 219*, 428*	,  ⊢
	: , : , :
191	instantiation	546, 655, 485, 548, 220, 549, 630, 223, 552, 260	⊢
	: , : , : , : , : , :
192	instantiation	490, 548, 657, 549, 221, 222, 630, 223, 552, 260, 224*	⊢
	: , : , : , : , : , :
193	instantiation	484, 225, 290	⊢
	: , :
194	instantiation	546, 548, 657, 655, 549, 226, 630, 426, 290	⊢
	: , : , : , : , : , :
195	instantiation	658, 591, 227	⊢
	: , : , :
196	instantiation	621, 228	,  ⊢
	: , : , :
197	instantiation	609, 229, 230	⊢
	: , : , :
198	instantiation	658, 585, 474	⊢
	: , : , :
199	instantiation	531, 231, 232	⊢
	: , : , :
200	instantiation	233, 234	,  ⊢
	: , :
201	instantiation	621, 235	⊢
	: , : , :
202	instantiation	621, 236	⊢
	: , : , :
203	instantiation	476, 381	⊢
	:
204	instantiation	609, 237, 238	⊢
	: , : , :
205	instantiation	609, 239, 240	⊢
	: , : , :
206	instantiation	609, 241, 242	,  ⊢
	: , : , :
207	instantiation	623, 274	,  ⊢
	:
208	instantiation	243, 244	,  ⊢
	:
209	instantiation	495, 245	⊢
	:
210	instantiation	596, 420, 394	⊢
	: , :
211	instantiation	546, 548, 657, 655, 549, 401, 630, 579, 370	⊢
	: , : , : , : , : , :
212	instantiation	621, 246	⊢
	: , : , :
213	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
214	instantiation	546, 655, 657, 548, 303, 549, 630, 579, 343	⊢
	: , : , : , : , : , :
215	instantiation	609, 247, 248	⊢
	: , : , :
216	instantiation	623, 282	⊢
	:
217	instantiation	596, 563, 449	⊢
	: , :
218	instantiation	506	⊢
	: , : , :
219	instantiation	555, 252, 628, 249*	⊢
	: , :
220	instantiation	506	⊢
	: , : , :
221	instantiation	604	⊢
	: , :
222	instantiation	604	⊢
	: , :
223	instantiation	250, 600, 529, 530	⊢
	: , :
224	instantiation	251, 630, 600, 566, 252, 611*, 253*	⊢
	: , : , : , :
225	instantiation	658, 636, 254	⊢
	: , : , :
226	instantiation	604	⊢
	: , :
227	instantiation	658, 607, 255	⊢
	: , : , :
228	instantiation	256, 299, 257, 630, 426, 290, 538, 584, 427, 258, 519*, 428*	,  ⊢
	: , : , :
229	instantiation	546, 655, 485, 548, 259, 549, 600, 521, 552, 260	⊢
	: , : , : , : , : , :
230	instantiation	547, 548, 485, 549, 259, 521, 552, 260	⊢
	: , : , : , :
231	instantiation	484, 368, 261	⊢
	: , :
232	instantiation	609, 262, 263	⊢
	: , : , :
233	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
234	instantiation	264, 265, 266, 267*	,  ⊢
	:
235	instantiation	621, 296	⊢
	: , : , :
236	instantiation	534, 351, 268, 269	⊢
	: , : , : , :
237	instantiation	489, 548, 657, 655, 549, 401, 630, 579, 381, 418	⊢
	: , : , : , : , : , : , :
238	instantiation	490, 655, 485, 548, 300, 549, 381, 630, 579, 418	⊢
	: , : , : , : , : , :
239	instantiation	621, 270	⊢
	: , : , :
240	instantiation	271, 329, 272*	⊢
	:
241	instantiation	621, 273	⊢
	: , : , :
242	instantiation	319, 567, 566, 274, 622*	,  ⊢
	: , : , :
243	theorem		⊢
	proveit.trigonometry.sine_pos_interval
244	instantiation	275, 438, 602, 304, 276	,  ⊢
	: , : , :
245	instantiation	509, 277, 278	⊢
	: , :
246	instantiation	609, 279, 280	⊢
	: , : , :
247	instantiation	621, 281	⊢
	: , : , :
248	instantiation	319, 377, 566, 282, 283*	⊢
	: , : , :
249	instantiation	582, 529	⊢
	:
250	theorem		⊢
	proveit.numbers.division.div_complex_closure
251	theorem		⊢
	proveit.numbers.division.prod_of_fracs
252	instantiation	658, 591, 284	⊢
	: , : , :
253	instantiation	609, 285, 286	⊢
	: , : , :
254	instantiation	596, 637, 449	⊢
	: , :
255	instantiation	658, 640, 287	⊢
	: , : , :
256	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_products
257	instantiation	506	⊢
	: , : , :
258	instantiation	288, 289	,  ⊢
	:
259	instantiation	506	⊢
	: , : , :
260	instantiation	509, 290, 510	⊢
	: , :
261	instantiation	484, 381, 418	⊢
	: , :
262	instantiation	546, 655, 657, 548, 291, 549, 368, 381, 418	⊢
	: , : , : , : , : , :
263	instantiation	546, 548, 657, 549, 401, 291, 630, 579, 381, 418	⊢
	: , : , : , : , : , :
264	theorem		⊢
	proveit.numbers.exponentiation.unit_complex_polar_num_neq_one
265	instantiation	531, 400, 375	⊢
	: , : , :
266	instantiation	292, 293, 294	,  ⊢
	: , : , :
267	instantiation	411, 295	⊢
	: , :
268	instantiation	411, 325	⊢
	: , :
269	instantiation	411, 296	⊢
	: , :
270	instantiation	433, 297	⊢
	:
271	theorem		⊢
	proveit.numbers.absolute_value.abs_even
272	instantiation	298, 299, 300, 630, 579, 418, 301*, 302*	⊢
	: , :
273	instantiation	490, 655, 657, 548, 303, 549, 630, 579, 343	⊢
	: , : , : , : , : , :
274	instantiation	658, 636, 304	,  ⊢
	: , : , :
275	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
276	instantiation	305, 306, 307	,  ⊢
	: , :
277	instantiation	658, 636, 308	⊢
	: , : , :
278	instantiation	531, 309, 310	⊢
	: , : , :
279	instantiation	489, 548, 657, 655, 549, 401, 630, 579, 381, 370	⊢
	: , : , : , : , : , : , :
280	instantiation	490, 655, 485, 548, 311, 549, 381, 630, 579, 370	⊢
	: , : , : , : , : , :
281	instantiation	609, 312, 313	⊢
	: , : , :
282	instantiation	658, 636, 314	⊢
	: , : , :
283	instantiation	629, 579	⊢
	:
284	instantiation	658, 607, 315	⊢
	: , : , :
285	instantiation	586, 657, 316, 317, 622, 318	⊢
	: , : , : , :
286	instantiation	319, 567, 600, 622*, 527*	⊢
	: , : , :
287	instantiation	658, 648, 474	⊢
	: , : , :
288	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_if_in_complex_nonzero
289	instantiation	531, 320, 321	,  ⊢
	: , : , :
290	instantiation	658, 636, 322	⊢
	: , : , :
291	instantiation	604	⊢
	: , :
292	theorem		⊢
	proveit.logic.equality.sub_left_side_into
293	instantiation	323, 460, 632, 461	,  ⊢
	: , :
294	instantiation	534, 324, 325, 326	⊢
	: , : , : , :
295	instantiation	621, 327	⊢
	: , : , :
296	instantiation	621, 328	⊢
	: , : , :
297	instantiation	495, 329	⊢
	:
298	theorem		⊢
	proveit.numbers.absolute_value.abs_prod
299	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
300	instantiation	506	⊢
	: , : , :
301	instantiation	331, 330	⊢
	:
302	instantiation	331, 332	⊢
	:
303	instantiation	604	⊢
	: , :
304	instantiation	333, 438, 363, 361	,  ⊢
	: , : , :
305	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
306	instantiation	334, 438, 363, 361	,  ⊢
	: , : , :
307	instantiation	335, 336, 337	,  ⊢
	: , : , :
308	instantiation	658, 616, 338	⊢
	: , : , :
309	instantiation	484, 368, 339	⊢
	: , :
310	instantiation	609, 340, 341	⊢
	: , : , :
311	instantiation	506	⊢
	: , : , :
312	instantiation	489, 548, 655, 549, 630, 579, 343	⊢
	: , : , : , : , : , : , :
313	instantiation	490, 655, 657, 548, 342, 549, 579, 630, 343	⊢
	: , : , : , : , : , :
314	instantiation	596, 637, 371	⊢
	: , :
315	instantiation	658, 640, 344	⊢
	: , : , :
316	instantiation	604	⊢
	: , :
317	instantiation	604	⊢
	: , :
318	instantiation	620, 529	⊢
	:
319	theorem		⊢
	proveit.numbers.division.frac_cancel_left
320	instantiation	658, 591, 345	,  ⊢
	: , : , :
321	instantiation	621, 351	⊢
	: , : , :
322	instantiation	658, 395, 346	⊢
	: , : , :
323	theorem		⊢
	proveit.physics.quantum.QPE._non_int_delta_b_diff
324	instantiation	477, 347, 368, 348, 349*	⊢
	: , :
325	instantiation	350, 471, 499	⊢
	: , :
326	instantiation	411, 351	⊢
	: , :
327	instantiation	609, 352, 353	⊢
	: , : , :
328	instantiation	609, 354, 355	⊢
	: , : , :
329	instantiation	531, 356, 357	⊢
	: , : , :
330	instantiation	358, 657	⊢
	:
331	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
332	instantiation	359, 387	⊢
	: , :
333	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
334	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
335	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
336	instantiation	360, 438, 363, 361	,  ⊢
	: , : , :
337	instantiation	362, 363, 364, 454, 365, 366*, 367*	⊢
	: , : , :
338	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
339	instantiation	484, 381, 370	⊢
	: , :
340	instantiation	546, 655, 657, 548, 369, 549, 368, 381, 370	⊢
	: , : , : , : , : , :
341	instantiation	546, 548, 657, 549, 401, 369, 630, 579, 381, 370	⊢
	: , : , : , : , : , :
342	instantiation	604	⊢
	: , :
343	instantiation	658, 636, 371	⊢
	: , : , :
344	instantiation	658, 648, 564	⊢
	: , : , :
345	instantiation	658, 576, 372	,  ⊢
	: , : , :
346	instantiation	416, 373	⊢
	:
347	instantiation	531, 374, 375	⊢
	: , : , :
348	instantiation	376, 657, 401, 567, 377	⊢
	: , :
349	instantiation	609, 378, 379	⊢
	: , : , :
350	theorem		⊢
	proveit.numbers.addition.commutation
351	instantiation	621, 380	⊢
	: , : , :
352	instantiation	489, 548, 657, 655, 549, 401, 630, 579, 381, 493	⊢
	: , : , : , : , : , : , :
353	instantiation	490, 655, 485, 548, 464, 549, 381, 630, 579, 493	⊢
	: , : , : , : , : , :
354	instantiation	621, 382	⊢
	: , : , :
355	instantiation	383, 548, 657, 549, 550, 600, 551, 552, 517*	⊢
	: , : , : , : , :
356	instantiation	658, 636, 384	⊢
	: , : , :
357	instantiation	546, 548, 657, 655, 549, 401, 630, 579, 418	⊢
	: , : , : , : , : , :
358	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
359	theorem		⊢
	proveit.numbers.ordering.relax_less
360	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
361	instantiation	385, 632, 461	,  ⊢
	:
362	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
363	instantiation	583, 602, 637, 584	⊢
	: , :
364	instantiation	596, 479, 438	⊢
	: , :
365	instantiation	386, 479, 438, 602, 387, 388	⊢
	: , : , :
366	instantiation	534, 389, 390, 391	⊢
	: , : , : , :
367	instantiation	609, 392, 393	⊢
	: , : , :
368	instantiation	658, 636, 420	⊢
	: , : , :
369	instantiation	604	⊢
	: , :
370	instantiation	658, 636, 394	⊢
	: , : , :
371	instantiation	658, 395, 396	⊢
	: , : , :
372	instantiation	397, 398	,  ⊢
	:
373	instantiation	399, 499, 471	⊢
	: , :
374	instantiation	658, 636, 400	⊢
	: , : , :
375	instantiation	546, 548, 657, 655, 549, 401, 630, 579, 493	⊢
	: , : , : , : , : , :
376	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
377	instantiation	658, 591, 543	⊢
	: , : , :
378	instantiation	621, 402	⊢
	: , : , :
379	instantiation	609, 403, 404	⊢
	: , : , :
380	instantiation	621, 405	⊢
	: , : , :
381	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
382	instantiation	621, 406	⊢
	: , : , :
383	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
384	instantiation	596, 420, 440	⊢
	: , :
385	theorem		⊢
	proveit.physics.quantum.QPE._scaled_abs_delta_b_floor_diff_interval
386	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
387	instantiation	407, 617	⊢
	:
388	instantiation	408, 523	⊢
	:
389	instantiation	609, 409, 410	⊢
	: , : , :
390	instantiation	615	⊢
	:
391	instantiation	411, 453	⊢
	: , :
392	instantiation	621, 453	⊢
	: , : , :
393	instantiation	411, 412, 413*	⊢
	: , :
394	instantiation	539, 414, 415	⊢
	: , :
395	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
396	instantiation	416, 418	⊢
	:
397	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
398	instantiation	417, 418, 419	,  ⊢
	:
399	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
400	instantiation	596, 420, 511	⊢
	: , :
401	instantiation	604	⊢
	: , :
402	instantiation	421, 630, 579, 538, 584, 513, 519*	⊢
	: , : , :
403	instantiation	609, 422, 423	⊢
	: , : , :
404	instantiation	609, 424, 425	⊢
	: , : , :
405	instantiation	477, 551, 426, 427, 428*	⊢
	: , :
406	instantiation	429, 600, 500, 430*	⊢
	: , :
407	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
408	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
409	instantiation	609, 431, 432	⊢
	: , : , :
410	instantiation	433, 434	⊢
	:
411	theorem		⊢
	proveit.logic.equality.equals_reversal
412	instantiation	469, 548, 657, 655, 549, 435, 521, 579	⊢
	: , : , : , : , : , :
413	instantiation	609, 436, 437	⊢
	: , : , :
414	instantiation	456, 438, 614, 439	⊢
	: , : , :
415	instantiation	572, 597	⊢
	:
416	theorem		⊢
	proveit.numbers.absolute_value.abs_complex_closure
417	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
418	instantiation	658, 636, 440	⊢
	: , : , :
419	instantiation	441, 442	,  ⊢
	: , :
420	instantiation	596, 637, 602	⊢
	: , :
421	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
422	instantiation	609, 443, 444	⊢
	: , : , :
423	instantiation	609, 445, 446	⊢
	: , : , :
424	instantiation	547, 548, 485, 549, 487, 579, 493, 492	⊢
	: , : , : , :
425	instantiation	609, 447, 448	⊢
	: , : , :
426	instantiation	658, 636, 449	⊢
	: , : , :
427	instantiation	603, 474	⊢
	:
428	instantiation	450, 630, 518, 538, 584, 451*	⊢
	: , : , :
429	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
430	instantiation	620, 500	⊢
	:
431	instantiation	621, 452	⊢
	: , : , :
432	instantiation	621, 453	⊢
	: , : , :
433	theorem		⊢
	proveit.numbers.addition.elim_zero_left
434	instantiation	658, 636, 454	⊢
	: , : , :
435	instantiation	604	⊢
	: , :
436	instantiation	621, 455	⊢
	: , : , :
437	instantiation	620, 579	⊢
	:
438	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
439	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
440	instantiation	456, 457, 557, 458	⊢
	: , : , :
441	theorem		⊢
	proveit.numbers.addition.subtraction.nonzero_difference_if_different
442	instantiation	459, 460, 624, 461	,  ⊢
	: , :
443	instantiation	546, 548, 485, 655, 549, 464, 630, 579, 493, 462	⊢
	: , : , : , : , : , :
444	instantiation	546, 485, 657, 548, 464, 463, 549, 630, 579, 493, 521, 492	⊢
	: , : , : , : , : , :
445	instantiation	489, 548, 485, 655, 549, 464, 630, 579, 493, 521, 492	⊢
	: , : , : , : , : , : , :
446	instantiation	609, 465, 466	⊢
	: , : , :
447	instantiation	609, 467, 468	⊢
	: , : , :
448	instantiation	469, 655, 657, 548, 470, 549, 600, 471, 499, 472*, 473*	⊢
	: , : , : , : , : , :
449	instantiation	553, 554, 474	⊢
	: , : , :
450	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
451	instantiation	496, 500, 600, 475*	⊢
	: , :
452	instantiation	476, 521	⊢
	:
453	instantiation	477, 579, 630, 584, 478*	⊢
	: , :
454	instantiation	596, 479, 602	⊢
	: , :
455	instantiation	480, 647, 652, 481*	⊢
	: , : , : , :
456	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
457	instantiation	572, 557	⊢
	:
458	instantiation	482, 632	⊢
	:
459	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_not_eq_scaledNonzeroInt
460	instantiation	483, 548, 655, 549	⊢
	: , : , : , : , :
461	assumption		⊢
462	instantiation	484, 521, 492	⊢
	: , :
463	instantiation	604	⊢
	: , :
464	instantiation	506	⊢
	: , : , :
465	instantiation	490, 548, 657, 485, 549, 486, 487, 521, 630, 579, 493, 492	⊢
	: , : , : , : , : , :
466	instantiation	621, 488	⊢
	: , : , :
467	instantiation	489, 655, 548, 549, 579, 493, 492	⊢
	: , : , : , : , : , : , :
468	instantiation	490, 548, 657, 655, 549, 491, 579, 492, 493, 494*	⊢
	: , : , : , : , : , :
469	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
470	instantiation	604	⊢
	: , :
471	instantiation	495, 497	⊢
	:
472	instantiation	496, 600, 497, 498*	⊢
	: , :
473	instantiation	620, 499	⊢
	:
474	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
475	instantiation	629, 500	⊢
	:
476	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
477	theorem		⊢
	proveit.numbers.division.div_as_mult
478	instantiation	609, 501, 502	⊢
	: , : , :
479	instantiation	658, 643, 503	⊢
	: , : , :
480	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
481	instantiation	609, 504, 505	⊢
	: , : , :
482	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_floor_diff_in_interval
483	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
484	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
485	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
486	instantiation	604	⊢
	: , :
487	instantiation	506	⊢
	: , : , :
488	instantiation	531, 507, 508	⊢
	: , : , :
489	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
490	theorem		⊢
	proveit.numbers.multiplication.association
491	instantiation	604	⊢
	: , :
492	instantiation	509, 579, 510	⊢
	: , :
493	instantiation	658, 636, 511	⊢
	: , : , :
494	instantiation	512, 579, 614, 538, 513, 514*, 515*	⊢
	: , : , :
495	theorem		⊢
	proveit.numbers.negation.complex_closure
496	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
497	instantiation	658, 636, 573	⊢
	: , : , :
498	instantiation	609, 516, 517	⊢
	: , : , :
499	instantiation	658, 636, 541	⊢
	: , : , :
500	instantiation	658, 636, 518	⊢
	: , : , :
501	instantiation	621, 519	⊢
	: , : , :
502	instantiation	520, 579, 521	⊢
	: , :
503	instantiation	658, 522, 523	⊢
	: , : , :
504	instantiation	586, 657, 524, 525, 526, 527	⊢
	: , : , : , :
505	instantiation	528, 529, 530	⊢
	:
506	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
507	instantiation	531, 532, 533	⊢
	: , : , :
508	instantiation	534, 535, 536, 537	⊢
	: , : , : , :
509	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
510	instantiation	658, 636, 538	⊢
	: , : , :
511	instantiation	539, 540, 541	⊢
	: , :
512	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
513	instantiation	542, 543	⊢
	:
514	instantiation	582, 579	⊢
	:
515	instantiation	609, 544, 545	⊢
	: , : , :
516	instantiation	546, 655, 657, 548, 550, 549, 600, 551, 552	⊢
	: , : , : , : , : , :
517	instantiation	547, 548, 657, 549, 550, 551, 552	⊢
	: , : , : , :
518	instantiation	553, 554, 650	⊢
	: , : , :
519	instantiation	555, 567, 628, 556*	⊢
	: , :
520	theorem		⊢
	proveit.numbers.multiplication.commutation
521	instantiation	658, 636, 557	⊢
	: , : , :
522	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
523	instantiation	558, 559, 560	⊢
	: , :
524	instantiation	604	⊢
	: , :
525	instantiation	604	⊢
	: , :
526	instantiation	609, 561, 562	⊢
	: , : , :
527	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
528	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
529	instantiation	658, 636, 563	⊢
	: , : , :
530	instantiation	603, 564	⊢
	:
531	theorem		⊢
	proveit.logic.equality.sub_right_side_into
532	instantiation	565, 600, 566, 567	⊢
	: , : , : , : , :
533	instantiation	609, 568, 569	⊢
	: , : , :
534	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
535	instantiation	621, 570	⊢
	: , : , :
536	instantiation	621, 570	⊢
	: , : , :
537	instantiation	629, 600	⊢
	:
538	instantiation	658, 643, 571	⊢
	: , : , :
539	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
540	instantiation	572, 573	⊢
	:
541	instantiation	574, 575	⊢
	:
542	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
543	instantiation	658, 576, 617	⊢
	: , : , :
544	instantiation	621, 577	⊢
	: , : , :
545	instantiation	578, 579	⊢
	:
546	theorem		⊢
	proveit.numbers.multiplication.disassociation
547	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
548	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
549	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
550	instantiation	604	⊢
	: , :
551	instantiation	658, 636, 597	⊢
	: , : , :
552	instantiation	658, 636, 598	⊢
	: , : , :
553	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
554	instantiation	580, 581	⊢
	: , :
555	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
556	instantiation	582, 630	⊢
	:
557	instantiation	583, 614, 637, 584	⊢
	: , :
558	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
559	instantiation	658, 585, 628	⊢
	: , : , :
560	instantiation	658, 585, 649	⊢
	: , : , :
561	instantiation	586, 657, 587, 588, 608, 622	⊢
	: , : , : , :
562	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
563	instantiation	658, 643, 589	⊢
	: , : , :
564	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
565	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
566	instantiation	658, 591, 590	⊢
	: , : , :
567	instantiation	658, 591, 592	⊢
	: , : , :
568	instantiation	621, 593	⊢
	: , : , :
569	instantiation	621, 594	⊢
	: , : , :
570	instantiation	623, 600	⊢
	:
571	instantiation	658, 651, 595	⊢
	: , : , :
572	theorem		⊢
	proveit.numbers.negation.real_closure
573	instantiation	596, 597, 598	⊢
	: , :
574	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
575	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
576	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
577	instantiation	599, 600, 601	⊢
	: , :
578	theorem		⊢
	proveit.numbers.exponentiation.exp_zero_eq_one
579	instantiation	658, 636, 602	⊢
	: , : , :
580	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
581	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
582	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
583	theorem		⊢
	proveit.numbers.division.div_real_closure
584	instantiation	603, 649	⊢
	:
585	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
586	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
587	instantiation	604	⊢
	: , :
588	instantiation	604	⊢
	: , :
589	instantiation	658, 651, 605	⊢
	: , : , :
590	instantiation	658, 607, 606	⊢
	: , : , :
591	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
592	instantiation	658, 607, 634	⊢
	: , : , :
593	instantiation	621, 608	⊢
	: , : , :
594	instantiation	609, 610, 611	⊢
	: , : , :
595	instantiation	653, 647	⊢
	:
596	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
597	instantiation	658, 643, 612	⊢
	: , : , :
598	instantiation	658, 643, 613	⊢
	: , : , :
599	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
600	instantiation	658, 636, 614	⊢
	: , : , :
601	instantiation	615	⊢
	:
602	instantiation	658, 616, 617	⊢
	: , : , :
603	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
604	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
605	instantiation	658, 656, 618	⊢
	: , : , :
606	instantiation	658, 640, 619	⊢
	: , : , :
607	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
608	instantiation	620, 630	⊢
	:
609	axiom		⊢
	proveit.logic.equality.equals_transitivity
610	instantiation	621, 622	⊢
	: , : , :
611	instantiation	623, 630	⊢
	:
612	instantiation	658, 651, 624	⊢
	: , : , :
613	instantiation	658, 625, 626	⊢
	: , : , :
614	instantiation	658, 643, 627	⊢
	: , : , :
615	axiom		⊢
	proveit.logic.equality.equals_reflexivity
616	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
617	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
618	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
619	instantiation	658, 648, 628	⊢
	: , : , :
620	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
621	axiom		⊢
	proveit.logic.equality.substitution
622	instantiation	629, 630	⊢
	:
623	theorem		⊢
	proveit.numbers.division.frac_one_denom
624	instantiation	658, 631, 632	⊢
	: , : , :
625	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
626	instantiation	633, 634, 635	⊢
	: , :
627	instantiation	658, 651, 647	⊢
	: , : , :
628	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
629	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
630	instantiation	658, 636, 637	⊢
	: , : , :
631	instantiation	638, 639, 654	⊢
	: , :
632	assumption		⊢
633	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
634	instantiation	658, 640, 641	⊢
	: , : , :
635	instantiation	653, 642	⊢
	:
636	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
637	instantiation	658, 643, 644	⊢
	: , : , :
638	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
639	instantiation	645, 646, 647	⊢
	: , :
640	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
641	instantiation	658, 648, 649	⊢
	: , : , :
642	instantiation	658, 659, 650	⊢
	: , : , :
643	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
644	instantiation	658, 651, 652	⊢
	: , : , :
645	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
646	instantiation	653, 654	⊢
	:
647	instantiation	658, 656, 655	⊢
	: , : , :
648	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
649	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
650	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
651	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
652	instantiation	658, 656, 657	⊢
	: , : , :
653	theorem		⊢
	proveit.numbers.negation.int_closure
654	instantiation	658, 659, 660	⊢
	: , : , :
655	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
656	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
657	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
658	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
659	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
660	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
*equality replacement requirements