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