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	318	⊢
2	instantiation	318, 4, 5	,  ⊢
	: , : , :
3	instantiation	281, 275, 417, 310, 6, 7, 311, 390, 351, 182, 142, 231, 8*	⊢
	: , : , : , : , : , :
4	instantiation	318, 9, 10, 11*	⊢
	: , : , :
5	instantiation	12, 32, 13, 14, 15, 16, 17*, 18*	,  ⊢
	: , : , : , :
6	instantiation	296	⊢
	: , : , :
7	instantiation	334	⊢
	: , :
8	instantiation	256, 310, 415, 311, 286, 196, 231, 19*	⊢
	: , : , : , : , : , :
9	instantiation	318, 20, 21, 22*	⊢
	: , : , :
10	instantiation	23, 409, 24, 119, 313, 231, 222	⊢
	: , : , :
11	instantiation	370, 25, 26	⊢
	: , : , :
12	theorem		⊢
	proveit.numbers.summation.gen_finite_geom_sum
13	instantiation	292, 27, 28	,  ⊢
	: , : , :
14	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
15	instantiation	405, 29, 359	⊢
	: , :
16	instantiation	30, 31	⊢
	: , :
17	instantiation	350, 32	⊢
	:
18	instantiation	370, 33, 34	⊢
	: , : , :
19	instantiation	318, 35, 36	⊢
	: , : , :
20	instantiation	292, 37, 38	⊢
	: , : , :
21	instantiation	39, 345	⊢
	:
22	instantiation	189, 310, 417, 415, 311, 63, 92, 286, 40	⊢
	: , : , : , : , : , :
23	theorem		⊢
	proveit.numbers.division.distribute_frac_through_sum
24	instantiation	334	⊢
	: , :
25	instantiation	381, 41	⊢
	: , : , :
26	instantiation	370, 42, 43	⊢
	: , : , :
27	instantiation	292, 44, 45	,  ⊢
	: , : , :
28	instantiation	381, 46	⊢
	: , : , :
29	instantiation	418, 419, 270	⊢
	: , : , :
30	theorem		⊢
	proveit.numbers.ordering.relax_less
31	instantiation	47, 48	⊢
	: , :
32	instantiation	301, 49, 52	⊢
	: , :
33	instantiation	381, 50	⊢
	: , : , :
34	instantiation	51, 108, 52, 231, 53*	⊢
	: , : , :
35	instantiation	318, 54, 55	⊢
	: , : , :
36	instantiation	321, 56, 57, 58	⊢
	: , : , : , :
37	instantiation	59, 173	⊢
	:
38	instantiation	60, 345, 384	⊢
	: , :
39	theorem		⊢
	proveit.physics.quantum.QPE._phase_from_best_with_delta_b
40	instantiation	195, 61	⊢
	:
41	instantiation	62, 92, 196	⊢
	: , :
42	instantiation	189, 417, 310, 63, 64, 311, 92, 286, 65, 170	⊢
	: , : , : , : , : , :
43	instantiation	66, 310, 415, 311, 92, 286, 170, 67	⊢
	: , : , : , : , : , : , : , :
44	instantiation	68, 69, 70, 71*	,  ⊢
	:
45	instantiation	381, 72	⊢
	: , : , :
46	instantiation	370, 73, 74	⊢
	: , : , :
47	theorem		⊢
	proveit.numbers.addition.subtraction.pos_difference
48	instantiation	75, 325, 99, 76, 77, 78*, 79*	⊢
	: , : , :
49	instantiation	418, 396, 80	⊢
	: , : , :
50	instantiation	370, 81, 82	⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.exponentiation.complex_power_of_complex_power
52	instantiation	318, 83, 84	⊢
	: , : , :
53	instantiation	308, 310, 85, 415, 311, 86, 390, 351, 182, 142, 231	⊢
	: , : , : , : , : , :
54	instantiation	337, 313, 364, 338, 87	⊢
	: , : , : , : , :
55	instantiation	370, 88, 89	⊢
	: , : , :
56	instantiation	381, 90	⊢
	: , : , :
57	instantiation	381, 342	⊢
	: , : , :
58	instantiation	389, 313	⊢
	:
59	theorem		⊢
	proveit.physics.quantum.QPE._alpha_m_mod_as_geometric_sum
60	axiom		⊢
	proveit.physics.quantum.QPE._mod_add_def
61	instantiation	297, 91, 231, 222	⊢
	: , :
62	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
63	instantiation	334	⊢
	: , :
64	instantiation	334	⊢
	: , :
65	instantiation	195, 92	⊢
	:
66	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
67	instantiation	376	⊢
	:
68	theorem		⊢
	proveit.numbers.exponentiation.unit_complex_polar_num_neq_one
69	instantiation	318, 197, 176	⊢
	: , : , :
70	instantiation	292, 93, 94	,  ⊢
	: , : , :
71	instantiation	265, 95	⊢
	: , :
72	instantiation	381, 156	⊢
	: , : , :
73	instantiation	280, 417, 415, 310, 198, 311, 390, 351, 182, 142	⊢
	: , : , : , : , : , : , :
74	instantiation	381, 96	⊢
	: , : , :
75	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
76	instantiation	418, 403, 97	⊢
	: , : , :
77	instantiation	98, 99, 100, 375, 101, 102	⊢
	: , : , :
78	instantiation	370, 103, 104	⊢
	: , : , :
79	instantiation	321, 105, 106, 107	⊢
	: , : , : , :
80	instantiation	418, 377, 108	⊢
	: , : , :
81	instantiation	189, 310, 417, 415, 311, 109, 231, 302, 364	⊢
	: , : , : , : , : , :
82	instantiation	110, 364, 231, 365	⊢
	: , : , :
83	instantiation	274, 150, 111	⊢
	: , :
84	instantiation	370, 112, 113	⊢
	: , : , :
85	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
86	instantiation	114	⊢
	: , : , : , :
87	instantiation	418, 355, 115	⊢
	: , : , :
88	instantiation	381, 116	⊢
	: , : , :
89	instantiation	381, 117	⊢
	: , : , :
90	instantiation	383, 313	⊢
	:
91	instantiation	418, 396, 118	⊢
	: , : , :
92	instantiation	297, 119, 231, 222	⊢
	: , :
93	instantiation	120, 121, 392, 122	,  ⊢
	: , :
94	instantiation	321, 123, 126, 124	⊢
	: , : , : , :
95	instantiation	381, 125	⊢
	: , : , :
96	instantiation	321, 153, 126, 127	⊢
	: , : , : , :
97	instantiation	418, 411, 128	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
99	instantiation	418, 403, 129	⊢
	: , : , :
100	instantiation	418, 377, 130	⊢
	: , : , :
101	instantiation	131, 397, 375, 132, 133, 134	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
103	instantiation	381, 382	⊢
	: , : , :
104	instantiation	135, 364, 390, 136	⊢
	: , : , :
105	instantiation	370, 137, 138	⊢
	: , : , :
106	instantiation	370, 139, 140	⊢
	: , : , :
107	instantiation	376	⊢
	:
108	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
109	instantiation	334	⊢
	: , :
110	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
111	instantiation	274, 182, 142	⊢
	: , :
112	instantiation	308, 415, 417, 310, 141, 311, 150, 182, 142	⊢
	: , : , : , : , : , :
113	instantiation	308, 310, 417, 311, 198, 141, 390, 351, 182, 142	⊢
	: , : , : , : , : , :
114	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
115	instantiation	418, 368, 143	⊢
	: , : , :
116	instantiation	381, 168	⊢
	: , : , :
117	instantiation	370, 144, 145	⊢
	: , : , :
118	instantiation	418, 403, 146	⊢
	: , : , :
119	instantiation	418, 396, 147	⊢
	: , : , :
120	theorem		⊢
	proveit.physics.quantum.QPE._non_int_delta_b_diff
121	instantiation	148, 310, 415, 311	⊢
	: , : , : , : , :
122	assumption		⊢
123	instantiation	221, 149, 150, 151, 152*	⊢
	: , :
124	instantiation	265, 153	⊢
	: , :
125	instantiation	370, 154, 155	⊢
	: , : , :
126	instantiation	376	⊢
	:
127	instantiation	265, 156	⊢
	: , :
128	instantiation	418, 416, 157	⊢
	: , : , :
129	instantiation	418, 411, 158	⊢
	: , : , :
130	instantiation	418, 159, 160	⊢
	: , : , :
131	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
132	instantiation	335, 336, 420	⊢
	: , : , :
133	instantiation	161, 420	⊢
	:
134	instantiation	162, 417	⊢
	:
135	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
136	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
137	instantiation	381, 163	⊢
	: , : , :
138	instantiation	370, 164, 165	⊢
	: , : , :
139	instantiation	381, 166	⊢
	: , : , :
140	instantiation	370, 167, 168	⊢
	: , : , :
141	instantiation	334	⊢
	: , :
142	instantiation	169, 286, 170	⊢
	: , :
143	instantiation	418, 400, 171	⊢
	: , : , :
144	instantiation	381, 172	⊢
	: , : , :
145	instantiation	383, 231	⊢
	:
146	instantiation	418, 411, 173	⊢
	: , : , :
147	instantiation	418, 403, 174	⊢
	: , : , :
148	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
149	instantiation	318, 175, 176	⊢
	: , : , :
150	instantiation	418, 396, 214	⊢
	: , : , :
151	instantiation	177, 417, 198, 339, 178	⊢
	: , :
152	instantiation	370, 179, 180	⊢
	: , : , :
153	instantiation	381, 181	⊢
	: , : , :
154	instantiation	280, 310, 275, 311, 251, 390, 351, 284, 182	⊢
	: , : , : , : , : , : , :
155	instantiation	281, 415, 275, 310, 251, 311, 182, 390, 351, 284	⊢
	: , : , : , : , : , :
156	instantiation	381, 183	⊢
	: , : , :
157	instantiation	184, 185, 415	⊢
	: , :
158	instantiation	418, 416, 186	⊢
	: , : , :
159	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
160	instantiation	418, 187, 206	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
162	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
163	instantiation	381, 188	⊢
	: , : , :
164	instantiation	189, 310, 417, 415, 311, 190, 192, 364, 302	⊢
	: , : , : , : , : , :
165	instantiation	191, 364, 192, 365	⊢
	: , : , :
166	instantiation	381, 293	⊢
	: , : , :
167	instantiation	370, 193, 194	⊢
	: , : , :
168	instantiation	380, 231	⊢
	:
169	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
170	instantiation	195, 196	⊢
	:
171	instantiation	418, 408, 270	⊢
	: , : , :
172	instantiation	389, 231	⊢
	:
173	instantiation	405, 345, 384	⊢
	: , :
174	instantiation	418, 411, 345	⊢
	: , : , :
175	instantiation	418, 396, 197	⊢
	: , : , :
176	instantiation	308, 310, 417, 415, 311, 198, 390, 351, 284	⊢
	: , : , : , : , : , :
177	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
178	instantiation	418, 355, 330	⊢
	: , : , :
179	instantiation	381, 199	⊢
	: , : , :
180	instantiation	370, 200, 201	⊢
	: , : , :
181	instantiation	381, 202	⊢
	: , : , :
182	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
183	instantiation	370, 203, 204	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
185	instantiation	418, 205, 206	⊢
	: , : , :
186	instantiation	207, 417, 415	⊢
	: , :
187	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
188	instantiation	370, 208, 209	⊢
	: , : , :
189	theorem		⊢
	proveit.numbers.addition.disassociation
190	instantiation	334	⊢
	: , :
191	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
192	instantiation	318, 210, 211	⊢
	: , : , :
193	instantiation	281, 310, 417, 415, 311, 212, 390, 278, 231	⊢
	: , : , : , : , : , :
194	instantiation	381, 213	⊢
	: , : , :
195	theorem		⊢
	proveit.numbers.negation.complex_closure
196	instantiation	297, 313, 231, 222	⊢
	: , :
197	instantiation	360, 214, 303	⊢
	: , :
198	instantiation	334	⊢
	: , :
199	instantiation	215, 390, 351, 325, 298, 305, 216*	⊢
	: , : , :
200	instantiation	370, 217, 218	⊢
	: , : , :
201	instantiation	370, 219, 220	⊢
	: , : , :
202	instantiation	221, 313, 231, 222, 223*	⊢
	: , :
203	instantiation	381, 224	⊢
	: , : , :
204	instantiation	225, 310, 417, 311, 312, 364, 313, 314, 288*	⊢
	: , : , : , : , :
205	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
206	instantiation	226, 409, 420	⊢
	: , :
207	theorem		⊢
	proveit.numbers.multiplication.mult_nat_closure_bin
208	instantiation	381, 227	⊢
	: , : , :
209	instantiation	308, 415, 417, 310, 228, 311, 390, 245, 231	⊢
	: , : , : , : , : , :
210	instantiation	274, 229, 231	⊢
	: , :
211	instantiation	308, 310, 417, 415, 311, 230, 390, 245, 231	⊢
	: , : , : , : , : , :
212	instantiation	334	⊢
	: , :
213	instantiation	318, 232, 300	⊢
	: , : , :
214	instantiation	360, 397, 366	⊢
	: , :
215	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
216	instantiation	291, 339, 388, 293*	⊢
	: , :
217	instantiation	370, 233, 234	⊢
	: , : , :
218	instantiation	370, 235, 236	⊢
	: , : , :
219	instantiation	309, 310, 275, 311, 277, 351, 284, 283	⊢
	: , : , : , :
220	instantiation	370, 237, 238	⊢
	: , : , :
221	theorem		⊢
	proveit.numbers.division.div_as_mult
222	instantiation	317, 270	⊢
	:
223	instantiation	239, 390, 315, 325, 298, 240*	⊢
	: , : , :
224	instantiation	381, 241	⊢
	: , : , :
225	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
226	theorem		⊢
	proveit.numbers.multiplication.mult_nat_pos_closure_bin
227	instantiation	321, 242, 243, 244	⊢
	: , : , : , :
228	instantiation	334	⊢
	: , :
229	instantiation	274, 390, 245	⊢
	: , :
230	instantiation	334	⊢
	: , :
231	instantiation	418, 396, 246	⊢
	: , : , :
232	instantiation	318, 247, 248	⊢
	: , : , :
233	instantiation	308, 310, 275, 415, 311, 251, 390, 351, 284, 249	⊢
	: , : , : , : , : , :
234	instantiation	308, 275, 417, 310, 251, 250, 311, 390, 351, 284, 278, 283	⊢
	: , : , : , : , : , :
235	instantiation	280, 310, 275, 415, 311, 251, 390, 351, 284, 278, 283	⊢
	: , : , : , : , : , : , :
236	instantiation	370, 252, 253	⊢
	: , : , :
237	instantiation	370, 254, 255	⊢
	: , : , :
238	instantiation	256, 415, 310, 311, 364, 286, 257, 258*, 259*	⊢
	: , : , : , : , : , :
239	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
240	instantiation	260, 290, 364, 261*	⊢
	: , :
241	instantiation	262, 364, 290, 263*	⊢
	: , :
242	instantiation	381, 264	⊢
	: , : , :
243	instantiation	265, 266	⊢
	: , :
244	instantiation	381, 267	⊢
	: , : , :
245	instantiation	297, 364, 268, 269	⊢
	: , :
246	instantiation	335, 336, 270	⊢
	: , : , :
247	instantiation	271, 364, 339, 338	⊢
	: , : , : , : , :
248	instantiation	370, 272, 273	⊢
	: , : , :
249	instantiation	274, 278, 283	⊢
	: , :
250	instantiation	334	⊢
	: , :
251	instantiation	296	⊢
	: , : , :
252	instantiation	281, 310, 417, 275, 311, 276, 277, 278, 390, 351, 284, 283	⊢
	: , : , : , : , : , :
253	instantiation	381, 279	⊢
	: , : , :
254	instantiation	280, 415, 310, 311, 351, 284, 283	⊢
	: , : , : , : , : , : , :
255	instantiation	281, 310, 417, 415, 311, 282, 351, 283, 284, 285*	⊢
	: , : , : , : , : , :
256	theorem		⊢
	proveit.numbers.multiplication.distribute_through_subtract
257	instantiation	418, 396, 347	⊢
	: , : , :
258	instantiation	380, 286	⊢
	:
259	instantiation	370, 287, 288	⊢
	: , : , :
260	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
261	instantiation	389, 290	⊢
	:
262	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
263	instantiation	380, 290	⊢
	:
264	instantiation	289, 290, 302	⊢
	: , :
265	theorem		⊢
	proveit.logic.equality.equals_reversal
266	instantiation	304, 390, 325, 315, 298	⊢
	: , : , :
267	instantiation	291, 339, 388	⊢
	: , :
268	instantiation	301, 390, 364	⊢
	: , :
269	instantiation	292, 298, 293	⊢
	: , : , :
270	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
271	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
272	instantiation	381, 294	⊢
	: , : , :
273	instantiation	381, 295	⊢
	: , : , :
274	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
275	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
276	instantiation	334	⊢
	: , :
277	instantiation	296	⊢
	: , : , :
278	instantiation	297, 364, 390, 298	⊢
	: , :
279	instantiation	318, 299, 300	⊢
	: , : , :
280	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
281	theorem		⊢
	proveit.numbers.multiplication.association
282	instantiation	334	⊢
	: , :
283	instantiation	301, 351, 302	⊢
	: , :
284	instantiation	418, 396, 303	⊢
	: , : , :
285	instantiation	304, 351, 375, 325, 305, 306*, 307*	⊢
	: , : , :
286	instantiation	418, 396, 327	⊢
	: , : , :
287	instantiation	308, 415, 417, 310, 312, 311, 364, 313, 314	⊢
	: , : , : , : , : , :
288	instantiation	309, 310, 417, 311, 312, 313, 314	⊢
	: , : , : , :
289	theorem		⊢
	proveit.numbers.addition.commutation
290	instantiation	418, 396, 315	⊢
	: , : , :
291	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
292	theorem		⊢
	proveit.logic.equality.sub_left_side_into
293	instantiation	331, 390	⊢
	:
294	instantiation	370, 316, 372	⊢
	: , : , :
295	instantiation	381, 382	⊢
	: , : , :
296	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
297	theorem		⊢
	proveit.numbers.division.div_complex_closure
298	instantiation	317, 409	⊢
	:
299	instantiation	318, 319, 320	⊢
	: , : , :
300	instantiation	321, 322, 323, 324	⊢
	: , : , : , :
301	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
302	instantiation	418, 396, 325	⊢
	: , : , :
303	instantiation	326, 327, 328	⊢
	: , :
304	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
305	instantiation	329, 330	⊢
	:
306	instantiation	331, 351	⊢
	:
307	instantiation	370, 332, 333	⊢
	: , : , :
308	theorem		⊢
	proveit.numbers.multiplication.disassociation
309	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
310	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
311	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
312	instantiation	334	⊢
	: , :
313	instantiation	418, 396, 361	⊢
	: , : , :
314	instantiation	418, 396, 362	⊢
	: , : , :
315	instantiation	335, 336, 410	⊢
	: , : , :
316	instantiation	381, 369	⊢
	: , : , :
317	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
318	theorem		⊢
	proveit.logic.equality.sub_right_side_into
319	instantiation	337, 364, 338, 339	⊢
	: , : , : , : , :
320	instantiation	370, 340, 341	⊢
	: , : , :
321	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
322	instantiation	381, 342	⊢
	: , : , :
323	instantiation	381, 342	⊢
	: , : , :
324	instantiation	389, 364	⊢
	:
325	instantiation	418, 403, 343	⊢
	: , : , :
326	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
327	instantiation	344, 345	⊢
	:
328	instantiation	346, 347	⊢
	:
329	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
330	instantiation	418, 348, 378	⊢
	: , : , :
331	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
332	instantiation	381, 349	⊢
	: , : , :
333	instantiation	350, 351	⊢
	:
334	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
335	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
336	instantiation	352, 353	⊢
	: , :
337	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
338	instantiation	418, 355, 354	⊢
	: , : , :
339	instantiation	418, 355, 356	⊢
	: , : , :
340	instantiation	381, 357	⊢
	: , : , :
341	instantiation	381, 358	⊢
	: , : , :
342	instantiation	383, 364	⊢
	:
343	instantiation	418, 411, 359	⊢
	: , : , :
344	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
345	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
346	theorem		⊢
	proveit.numbers.negation.real_closure
347	instantiation	360, 361, 362	⊢
	: , :
348	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
349	instantiation	363, 364, 365	⊢
	: , :
350	theorem		⊢
	proveit.numbers.exponentiation.exp_zero_eq_one
351	instantiation	418, 396, 366	⊢
	: , : , :
352	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
353	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
354	instantiation	418, 368, 367	⊢
	: , : , :
355	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
356	instantiation	418, 368, 394	⊢
	: , : , :
357	instantiation	381, 369	⊢
	: , : , :
358	instantiation	370, 371, 372	⊢
	: , : , :
359	instantiation	413, 407	⊢
	:
360	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
361	instantiation	418, 403, 373	⊢
	: , : , :
362	instantiation	418, 403, 374	⊢
	: , : , :
363	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
364	instantiation	418, 396, 375	⊢
	: , : , :
365	instantiation	376	⊢
	:
366	instantiation	418, 377, 378	⊢
	: , : , :
367	instantiation	418, 400, 379	⊢
	: , : , :
368	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
369	instantiation	380, 390	⊢
	:
370	axiom		⊢
	proveit.logic.equality.equals_transitivity
371	instantiation	381, 382	⊢
	: , : , :
372	instantiation	383, 390	⊢
	:
373	instantiation	418, 411, 384	⊢
	: , : , :
374	instantiation	418, 385, 386	⊢
	: , : , :
375	instantiation	418, 403, 387	⊢
	: , : , :
376	axiom		⊢
	proveit.logic.equality.equals_reflexivity
377	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
378	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
379	instantiation	418, 408, 388	⊢
	: , : , :
380	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
381	axiom		⊢
	proveit.logic.equality.substitution
382	instantiation	389, 390	⊢
	:
383	theorem		⊢
	proveit.numbers.division.frac_one_denom
384	instantiation	418, 391, 392	⊢
	: , : , :
385	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
386	instantiation	393, 394, 395	⊢
	: , :
387	instantiation	418, 411, 407	⊢
	: , : , :
388	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
389	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
390	instantiation	418, 396, 397	⊢
	: , : , :
391	instantiation	398, 399, 414	⊢
	: , :
392	assumption		⊢
393	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
394	instantiation	418, 400, 401	⊢
	: , : , :
395	instantiation	413, 402	⊢
	:
396	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
397	instantiation	418, 403, 404	⊢
	: , : , :
398	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
399	instantiation	405, 406, 407	⊢
	: , :
400	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
401	instantiation	418, 408, 409	⊢
	: , : , :
402	instantiation	418, 419, 410	⊢
	: , : , :
403	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
404	instantiation	418, 411, 412	⊢
	: , : , :
405	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
406	instantiation	413, 414	⊢
	:
407	instantiation	418, 416, 415	⊢
	: , : , :
408	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
409	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
410	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
411	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
412	instantiation	418, 416, 417	⊢
	: , : , :
413	theorem		⊢
	proveit.numbers.negation.int_closure
414	instantiation	418, 419, 420	⊢
	: , : , :
415	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
416	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
417	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
418	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
419	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
420	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
*equality replacement requirements