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