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