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