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