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