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	330	⊢
2	instantiation	77, 4, 5	⊢
	: , : , :
3	instantiation	373, 6, 7, 8*	⊢
	: , : , :
4	instantiation	330, 9, 10	⊢
	: , : , :
5	instantiation	43, 60, 61, 39	⊢
	: , : , :
6	instantiation	371, 11	⊢
	: , : , :
7	instantiation	290, 12	⊢
	: , :
8	instantiation	373, 13, 55	⊢
	: , : , :
9	instantiation	330, 14, 15	⊢
	: , : , :
10	instantiation	371, 16	⊢
	: , : , :
11	instantiation	275, 17, 18, 19	⊢
	: , : , : , :
12	instantiation	20, 407, 21, 173, 22, 23*, 24*	⊢
	: , : , : , :
13	instantiation	371, 331	⊢
	: , : , :
14	instantiation	77, 25, 26	⊢
	: , : , :
15	instantiation	317, 455, 452, 388, 27, 389, 386, 28, 29, 30*	⊢
	: , : , : , : , : , :
16	instantiation	373, 31, 32	⊢
	: , : , :
17	instantiation	371, 33	⊢
	: , : , :
18	instantiation	385, 388, 452, 455, 389, 34, 407, 38, 39	⊢
	: , : , : , : , : , :
19	instantiation	35, 455, 452, 388, 36, 389, 407, 38, 39	⊢
	: , : , : , : , : , :
20	theorem		⊢
	proveit.numbers.division.prod_of_fracs
21	instantiation	37, 38, 39	⊢
	: , :
22	instantiation	75, 41, 40	⊢
	:
23	instantiation	214, 407	⊢
	:
24	instantiation	225, 41	⊢
	:
25	instantiation	330, 42, 95	⊢
	: , : , :
26	instantiation	43, 44, 386, 45*	⊢
	: , : , :
27	instantiation	404	⊢
	: , :
28	instantiation	453, 424, 46	⊢
	: , : , :
29	instantiation	453, 424, 47	⊢
	: , : , :
30	instantiation	330, 48, 49	⊢
	: , : , :
31	instantiation	315, 388, 452, 455, 389, 50, 415, 177, 386	⊢
	: , : , : , : , : , :
32	instantiation	373, 51, 52	⊢
	: , : , :
33	instantiation	53, 410, 425, 434, 72, 54, 55*	⊢
	: , : , : , :
34	instantiation	404	⊢
	: , :
35	theorem		⊢
	proveit.numbers.multiplication.association
36	instantiation	404	⊢
	: , :
37	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
38	instantiation	406, 407, 56	⊢
	: , :
39	instantiation	453, 424, 57	⊢
	: , : , :
40	instantiation	58, 452, 59, 60, 61	⊢
	: , :
41	instantiation	453, 424, 62	⊢
	: , : , :
42	instantiation	77, 63, 64	⊢
	: , : , :
43	theorem		⊢
	proveit.numbers.division.frac_cancel_left
44	instantiation	453, 412, 157	⊢
	: , : , :
45	instantiation	373, 65, 66	⊢
	: , : , :
46	instantiation	430, 105	⊢
	:
47	instantiation	430, 106	⊢
	:
48	instantiation	290, 67	⊢
	: , :
49	instantiation	371, 68	⊢
	: , : , :
50	instantiation	404	⊢
	: , :
51	instantiation	266, 455, 388, 389, 415, 177, 386	⊢
	: , : , : , : , : , : , :
52	instantiation	317, 388, 452, 455, 389, 69, 415, 386, 177, 70*	⊢
	: , : , : , : , : , :
53	theorem		⊢
	proveit.numbers.exponentiation.exp_factored_real
54	instantiation	290, 71	⊢
	: , :
55	instantiation	414, 407	⊢
	:
56	instantiation	453, 424, 72	⊢
	: , : , :
57	instantiation	273, 73, 199	⊢
	: , :
58	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
59	instantiation	404	⊢
	: , :
60	instantiation	74, 174, 415	⊢
	: , :
61	instantiation	75, 109, 124	⊢
	:
62	instantiation	187, 76, 125	⊢
	: , :
63	instantiation	77, 78, 79	⊢
	: , : , :
64	instantiation	80, 415, 81, 449	⊢
	: , : , :
65	instantiation	82, 452, 83, 84, 85, 86	⊢
	: , : , : , :
66	instantiation	371, 87	⊢
	: , : , :
67	instantiation	88, 89, 90	⊢
	: , :
68	instantiation	290, 91	⊢
	: , :
69	instantiation	404	⊢
	: , :
70	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
71	instantiation	373, 92, 340	⊢
	: , : , :
72	instantiation	273, 425, 418	⊢
	: , :
73	instantiation	453, 443, 93	⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_nonzero_closure
75	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
76	instantiation	205, 420, 452	⊢
	: , :
77	theorem		⊢
	proveit.logic.equality.sub_left_side_into
78	instantiation	330, 94, 95	⊢
	: , : , :
79	instantiation	275, 96, 97, 98	⊢
	: , : , : , :
80	theorem		⊢
	proveit.numbers.exponentiation.posnat_power_of_product
81	instantiation	453, 424, 228	⊢
	: , : , :
82	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
83	instantiation	404	⊢
	: , :
84	instantiation	404	⊢
	: , :
85	instantiation	99, 141, 386	⊢
	: , :
86	instantiation	100, 141, 447, 101*, 340*	⊢
	: , : , :
87	instantiation	275, 102, 103, 104	⊢
	: , : , : , :
88	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
89	instantiation	453, 424, 105	⊢
	: , : , :
90	instantiation	453, 424, 106	⊢
	: , : , :
91	instantiation	107, 449, 108, 141, 386, 109, 124	⊢
	: , : , :
92	instantiation	371, 331	⊢
	: , : , :
93	instantiation	453, 450, 110	⊢
	: , : , :
94	instantiation	250, 111, 112	⊢
	: , : , :
95	instantiation	113, 455, 452, 388, 114, 389, 415, 386, 268, 115*, 116*	⊢
	: , : , : , : , : , :
96	instantiation	117, 449, 415	⊢
	: , :
97	instantiation	118, 452, 119, 120, 121	⊢
	: , : , : , :
98	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
99	theorem		⊢
	proveit.numbers.multiplication.commutation
100	theorem		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
101	instantiation	414, 141	⊢
	:
102	instantiation	373, 122, 123	⊢
	: , : , :
103	instantiation	326	⊢
	:
104	instantiation	290, 138	⊢
	: , :
105	instantiation	215, 156, 125, 124	⊢
	: , :
106	instantiation	215, 434, 125, 124	⊢
	: , :
107	theorem		⊢
	proveit.numbers.division.distribute_frac_through_sum
108	instantiation	404	⊢
	: , :
109	instantiation	453, 424, 125	⊢
	: , : , :
110	instantiation	453, 454, 126	⊢
	: , : , :
111	instantiation	130, 452, 388, 127, 389, 434, 128, 129	⊢
	: , : , : , : , : , :
112	instantiation	130, 455, 434, 131, 132	⊢
	: , : , : , : , : , :
113	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
114	instantiation	404	⊢
	: , :
115	instantiation	133, 415	⊢
	:
116	instantiation	330, 134, 135	⊢
	: , : , :
117	theorem		⊢
	proveit.numbers.exponentiation.exp_nat_pos_expansion
118	theorem		⊢
	proveit.core_expr_types.operations.operands_substitution_via_tuple
119	instantiation	136, 452	⊢
	: , :
120	instantiation	404	⊢
	: , :
121	instantiation	137	⊢
	:
122	instantiation	371, 138	⊢
	: , : , :
123	instantiation	225, 139	⊢
	:
124	instantiation	140, 141, 415, 142	⊢
	: , :
125	instantiation	205, 156, 452	⊢
	: , :
126	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
127	instantiation	404	⊢
	: , :
128	instantiation	430, 148	⊢
	:
129	instantiation	146, 145, 143, 144	⊢
	: , :
130	theorem		⊢
	proveit.numbers.addition.weak_bound_via_term_bound
131	instantiation	430, 145	⊢
	:
132	instantiation	146, 147, 148, 149	⊢
	: , :
133	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
134	instantiation	330, 150, 151	⊢
	: , : , :
135	instantiation	373, 152, 153	⊢
	: , : , :
136	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
137	theorem		⊢
	proveit.numbers.numerals.decimals.reduce_2_repeats
138	instantiation	371, 154	⊢
	: , : , :
139	instantiation	155, 415, 392	⊢
	: , :
140	theorem		⊢
	proveit.numbers.exponentiation.exp_not_eq_zero
141	instantiation	453, 424, 156	⊢
	: , : , :
142	instantiation	359, 157	⊢
	:
143	instantiation	215, 434, 158, 159	⊢
	: , :
144	instantiation	168, 169, 201, 160, 161	⊢
	: , : , :
145	instantiation	215, 434, 162, 163	⊢
	: , :
146	theorem		⊢
	proveit.numbers.negation.negated_weak_bound
147	instantiation	215, 434, 164, 165	⊢
	: , :
148	instantiation	215, 434, 166, 167	⊢
	: , :
149	instantiation	168, 169, 209, 170, 171	⊢
	: , : , :
150	instantiation	172, 386, 402, 173, 174	⊢
	: , : , : , : , :
151	instantiation	371, 175	⊢
	: , : , :
152	instantiation	371, 176	⊢
	: , : , :
153	instantiation	225, 177	⊢
	:
154	instantiation	348, 386, 407, 383, 178*	⊢
	: , :
155	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
156	instantiation	273, 425, 199	⊢
	: , :
157	instantiation	453, 369, 179	⊢
	: , : , :
158	instantiation	187, 184, 181	⊢
	: , :
159	instantiation	359, 180	⊢
	:
160	instantiation	453, 440, 206	⊢
	: , : , :
161	instantiation	193, 184, 181, 185, 182, 183	⊢
	: , : , :
162	instantiation	187, 184, 185	⊢
	: , :
163	instantiation	188, 186	⊢
	:
164	instantiation	187, 425, 282	⊢
	: , :
165	instantiation	188, 189	⊢
	:
166	instantiation	453, 416, 209	⊢
	: , : , :
167	instantiation	359, 190	⊢
	:
168	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
169	instantiation	453, 191, 192	⊢
	: , : , :
170	instantiation	453, 440, 208	⊢
	: , : , :
171	instantiation	193, 425, 228, 282, 220, 194	⊢
	: , : , :
172	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
173	instantiation	453, 412, 195	⊢
	: , : , :
174	instantiation	453, 412, 196	⊢
	: , : , :
175	instantiation	373, 197, 198	⊢
	: , : , :
176	instantiation	214, 386	⊢
	:
177	instantiation	453, 424, 199	⊢
	: , : , :
178	instantiation	225, 392	⊢
	:
179	instantiation	376, 428, 200	⊢
	: , :
180	instantiation	453, 369, 201	⊢
	: , : , :
181	instantiation	205, 228, 452	⊢
	: , :
182	instantiation	202, 425, 228, 282, 203, 284	⊢
	: , : , :
183	instantiation	211, 235	⊢
	:
184	instantiation	453, 443, 204	⊢
	: , : , :
185	instantiation	205, 282, 452	⊢
	: , :
186	instantiation	453, 207, 206	⊢
	: , : , :
187	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
188	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_if_in_rational_nonzero
189	instantiation	453, 207, 208	⊢
	: , : , :
190	instantiation	453, 369, 209	⊢
	: , : , :
191	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
192	instantiation	453, 210, 455	⊢
	: , : , :
193	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
194	instantiation	211, 452	⊢
	:
195	instantiation	453, 422, 212	⊢
	: , : , :
196	instantiation	453, 369, 410	⊢
	: , : , :
197	instantiation	371, 213	⊢
	: , : , :
198	instantiation	214, 415	⊢
	:
199	instantiation	215, 434, 420, 383	⊢
	: , :
200	instantiation	426, 427, 410, 383	⊢
	: , :
201	instantiation	393, 216, 217	⊢
	: , :
202	theorem		⊢
	proveit.numbers.exponentiation.exp_pos_lesseq
203	instantiation	218, 219, 220	⊢
	: , :
204	instantiation	453, 450, 221	⊢
	: , : , :
205	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
206	instantiation	223, 226, 222	⊢
	: , :
207	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
208	instantiation	223, 441, 237	⊢
	: , :
209	instantiation	393, 428, 249	⊢
	: , :
210	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
211	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
212	instantiation	453, 436, 224	⊢
	: , : , :
213	instantiation	225, 415	⊢
	:
214	theorem		⊢
	proveit.numbers.division.frac_one_denom
215	theorem		⊢
	proveit.numbers.division.div_real_closure
216	instantiation	453, 440, 226	⊢
	: , : , :
217	instantiation	227, 228, 229	⊢
	:
218	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
219	instantiation	230, 231	⊢
	:
220	instantiation	260, 418, 232, 329, 233, 234*	⊢
	: , : , :
221	instantiation	453, 454, 235	⊢
	: , : , :
222	instantiation	236, 237, 446	⊢
	: , :
223	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
224	instantiation	453, 445, 447	⊢
	: , : , :
225	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
226	instantiation	453, 448, 238	⊢
	: , : , :
227	theorem		⊢
	proveit.numbers.exponentiation.sqrd_pos_closure
228	instantiation	273, 434, 279	⊢
	: , :
229	instantiation	359, 239	⊢
	:
230	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
231	instantiation	453, 240, 249	⊢
	: , : , :
232	instantiation	453, 416, 321	⊢
	: , : , :
233	instantiation	241, 425, 307, 242, 396, 243, 244*	⊢
	: , : , :
234	instantiation	373, 245, 246	⊢
	: , : , :
235	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
236	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_pos_closure
237	instantiation	247, 291, 248	⊢
	:
238	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
239	instantiation	453, 369, 249	⊢
	: , : , :
240	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonneg
241	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
242	instantiation	273, 263, 261	⊢
	: , :
243	instantiation	250, 251, 252	⊢
	: , : , :
244	instantiation	253, 428, 321, 365	⊢
	: , :
245	instantiation	315, 388, 452, 455, 389, 254, 415, 268, 408	⊢
	: , : , : , : , : , :
246	instantiation	373, 255, 256	⊢
	: , : , :
247	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.pos_rational_is_rational_pos
248	instantiation	257, 258	⊢
	: , :
249	instantiation	376, 427, 333	⊢
	: , :
250	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
251	instantiation	259, 307	⊢
	:
252	instantiation	260, 261, 262, 263, 264, 265*	⊢
	: , : , :
253	theorem		⊢
	proveit.numbers.exponentiation.exponent_log_with_same_base
254	instantiation	404	⊢
	: , :
255	instantiation	266, 455, 388, 389, 415, 268, 408	⊢
	: , : , : , : , : , : , :
256	instantiation	317, 388, 452, 455, 389, 267, 415, 408, 268, 331*	⊢
	: , : , : , : , : , :
257	theorem		⊢
	proveit.numbers.addition.subtraction.pos_difference
258	instantiation	269, 418, 425, 270, 271, 331*, 272*	⊢
	: , : , :
259	theorem		⊢
	proveit.numbers.rounding.ceil_x_ge_x
260	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
261	instantiation	430, 335	⊢
	:
262	instantiation	273, 335, 274	⊢
	: , :
263	instantiation	343, 344, 379	⊢
	: , : , :
264	axiom		⊢
	proveit.physics.quantum.QPE._t_req
265	instantiation	275, 276, 277, 278	⊢
	: , : , : , :
266	theorem		⊢
	proveit.numbers.addition.leftward_commutation
267	instantiation	404	⊢
	: , :
268	instantiation	453, 424, 279	⊢
	: , : , :
269	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
270	instantiation	453, 443, 280	⊢
	: , : , :
271	instantiation	281, 425, 282, 283, 284	⊢
	: , : , :
272	instantiation	373, 285, 286	⊢
	: , : , :
273	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
274	instantiation	453, 443, 287	⊢
	: , : , :
275	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
276	instantiation	373, 288, 289	⊢
	: , : , :
277	instantiation	326	⊢
	:
278	instantiation	290, 308	⊢
	: , :
279	instantiation	453, 416, 333	⊢
	: , : , :
280	instantiation	300, 291, 438	⊢
	: , :
281	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
282	instantiation	453, 443, 291	⊢
	: , : , :
283	theorem		⊢
	proveit.physics.quantum.QPE._e_value_ge_two
284	instantiation	292, 449	⊢
	:
285	instantiation	371, 293	⊢
	: , : , :
286	instantiation	373, 294, 295	⊢
	: , : , :
287	instantiation	453, 450, 296	⊢
	: , : , :
288	instantiation	371, 297	⊢
	: , : , :
289	instantiation	373, 298, 299	⊢
	: , : , :
290	theorem		⊢
	proveit.logic.equality.equals_reversal
291	instantiation	300, 338, 301	⊢
	: , :
292	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
293	instantiation	373, 302, 303	⊢
	: , : , :
294	instantiation	315, 388, 452, 455, 389, 304, 319, 386, 408	⊢
	: , : , : , : , : , :
295	instantiation	305, 386, 319, 306	⊢
	: , : , :
296	instantiation	354, 307	⊢
	:
297	instantiation	371, 308	⊢
	: , : , :
298	instantiation	315, 388, 452, 455, 389, 309, 324, 312, 310	⊢
	: , : , : , : , : , :
299	instantiation	311, 324, 312, 313	⊢
	: , : , :
300	theorem		⊢
	proveit.numbers.addition.add_rational_closure_bin
301	instantiation	453, 450, 314	⊢
	: , : , :
302	instantiation	315, 388, 452, 455, 389, 316, 319, 408, 415	⊢
	: , : , : , : , : , :
303	instantiation	317, 455, 452, 388, 318, 389, 319, 408, 415, 320*	⊢
	: , : , : , : , : , :
304	instantiation	404	⊢
	: , :
305	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
306	instantiation	326	⊢
	:
307	instantiation	363, 428, 321, 365	⊢
	: , :
308	instantiation	371, 322	⊢
	: , : , :
309	instantiation	404	⊢
	: , :
310	instantiation	323, 324	⊢
	:
311	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
312	instantiation	453, 424, 325	⊢
	: , : , :
313	instantiation	326	⊢
	:
314	instantiation	453, 327, 328	⊢
	: , : , :
315	theorem		⊢
	proveit.numbers.addition.disassociation
316	instantiation	404	⊢
	: , :
317	theorem		⊢
	proveit.numbers.addition.association
318	instantiation	404	⊢
	: , :
319	instantiation	453, 424, 329	⊢
	: , : , :
320	instantiation	330, 331, 332	⊢
	: , : , :
321	instantiation	376, 428, 333	⊢
	: , :
322	instantiation	371, 334	⊢
	: , : , :
323	theorem		⊢
	proveit.numbers.negation.complex_closure
324	instantiation	453, 424, 335	⊢
	: , : , :
325	instantiation	453, 443, 336	⊢
	: , : , :
326	axiom		⊢
	proveit.logic.equality.equals_reflexivity
327	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
328	instantiation	337, 447	⊢
	:
329	instantiation	453, 443, 338	⊢
	: , : , :
330	theorem		⊢
	proveit.logic.equality.sub_right_side_into
331	instantiation	339, 386, 415, 340	⊢
	: , : , :
332	instantiation	341, 415, 408	⊢
	: , :
333	instantiation	426, 427, 370, 350	⊢
	: , :
334	instantiation	371, 342	⊢
	: , : , :
335	instantiation	343, 344, 398	⊢
	: , : , :
336	instantiation	453, 450, 345	⊢
	: , : , :
337	theorem		⊢
	proveit.numbers.negation.int_neg_closure
338	instantiation	453, 346, 347	⊢
	: , : , :
339	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
340	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
341	theorem		⊢
	proveit.numbers.addition.commutation
342	instantiation	348, 386, 349, 350, 351*	⊢
	: , :
343	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
344	instantiation	352, 353	⊢
	: , :
345	instantiation	354, 355	⊢
	:
346	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
347	instantiation	356, 423, 357	⊢
	: , :
348	theorem		⊢
	proveit.numbers.division.div_as_mult
349	instantiation	453, 424, 358	⊢
	: , : , :
350	instantiation	359, 360	⊢
	:
351	instantiation	373, 361, 362	⊢
	: , : , :
352	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
353	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
354	axiom		⊢
	proveit.numbers.rounding.ceil_is_an_int
355	instantiation	363, 428, 364, 365	⊢
	: , :
356	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
357	instantiation	366, 367, 368	⊢
	: , :
358	instantiation	453, 416, 370	⊢
	: , : , :
359	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
360	instantiation	453, 369, 370	⊢
	: , : , :
361	instantiation	371, 372	⊢
	: , : , :
362	instantiation	373, 374, 375	⊢
	: , : , :
363	theorem		⊢
	proveit.numbers.logarithms.log_real_pos_real_closure
364	instantiation	376, 428, 377	⊢
	: , :
365	instantiation	399, 378	⊢
	: , :
366	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
367	instantiation	453, 397, 379	⊢
	: , : , :
368	instantiation	380, 381	⊢
	:
369	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
370	instantiation	393, 428, 410	⊢
	: , :
371	axiom		⊢
	proveit.logic.equality.substitution
372	instantiation	382, 415, 407, 418, 429, 383, 384*	⊢
	: , : , :
373	axiom		⊢
	proveit.logic.equality.equals_transitivity
374	instantiation	385, 455, 452, 388, 390, 389, 386, 391, 392	⊢
	: , : , : , : , : , :
375	instantiation	387, 388, 452, 389, 390, 391, 392	⊢
	: , : , : , :
376	theorem		⊢
	proveit.numbers.addition.add_real_pos_closure_bin
377	instantiation	393, 417, 394	⊢
	: , :
378	instantiation	395, 455, 452, 396	⊢
	: , :
379	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
380	theorem		⊢
	proveit.numbers.negation.int_closure
381	instantiation	453, 397, 398	⊢
	: , : , :
382	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
383	instantiation	399, 400	⊢
	: , :
384	instantiation	401, 402, 447, 403*	⊢
	: , :
385	theorem		⊢
	proveit.numbers.multiplication.disassociation
386	instantiation	453, 424, 434	⊢
	: , : , :
387	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
388	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
389	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
390	instantiation	404	⊢
	: , :
391	instantiation	453, 424, 405	⊢
	: , : , :
392	instantiation	406, 407, 408	⊢
	: , :
393	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
394	instantiation	409, 410, 418	⊢
	: , :
395	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
396	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
397	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
398	axiom		⊢
	proveit.physics.quantum.QPE._n_in_natural_pos
399	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
400	instantiation	411, 433, 420, 421	⊢
	: , :
401	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
402	instantiation	453, 412, 413	⊢
	: , : , :
403	instantiation	414, 415	⊢
	:
404	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
405	instantiation	453, 416, 417	⊢
	: , : , :
406	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
407	instantiation	453, 424, 420	⊢
	: , : , :
408	instantiation	453, 424, 418	⊢
	: , : , :
409	theorem		⊢
	proveit.numbers.exponentiation.exp_real_pos_closure
410	instantiation	419, 420, 421	⊢
	:
411	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq
412	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
413	instantiation	453, 422, 423	⊢
	: , : , :
414	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
415	instantiation	453, 424, 425	⊢
	: , : , :
416	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
417	instantiation	426, 427, 428, 429	⊢
	: , :
418	instantiation	430, 434	⊢
	:
419	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
420	instantiation	431, 433, 434, 435	⊢
	: , : , :
421	instantiation	432, 433, 434, 435	⊢
	: , : , :
422	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
423	instantiation	453, 436, 437	⊢
	: , : , :
424	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
425	instantiation	453, 443, 438	⊢
	: , : , :
426	theorem		⊢
	proveit.numbers.division.div_real_pos_closure
427	instantiation	453, 440, 439	⊢
	: , : , :
428	instantiation	453, 440, 441	⊢
	: , : , :
429	instantiation	442, 449	⊢
	:
430	theorem		⊢
	proveit.numbers.negation.real_closure
431	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
432	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
433	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
434	instantiation	453, 443, 444	⊢
	: , : , :
435	axiom		⊢
	proveit.physics.quantum.QPE._eps_in_interval
436	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
437	instantiation	453, 445, 449	⊢
	: , : , :
438	instantiation	453, 450, 446	⊢
	: , : , :
439	instantiation	453, 448, 447	⊢
	: , : , :
440	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
441	instantiation	453, 448, 449	⊢
	: , : , :
442	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
443	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
444	instantiation	453, 450, 451	⊢
	: , : , :
445	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
446	instantiation	453, 454, 452	⊢
	: , : , :
447	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
448	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
449	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
450	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
451	instantiation	453, 454, 455	⊢
	: , : , :
452	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
453	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
454	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
455	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements