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	4	⊢
2	instantiation	4, 5, 6	⊢
	: , : , :
3	instantiation	7, 301, 8, 335	⊢
	: , : , :
4	theorem		⊢
	proveit.logic.equality.sub_left_side_into
5	instantiation	216, 9, 10	⊢
	: , : , :
6	instantiation	161, 11, 12, 13	⊢
	: , : , : , :
7	theorem		⊢
	proveit.numbers.exponentiation.posnat_power_of_product
8	instantiation	339, 310, 114	⊢
	: , : , :
9	instantiation	136, 14, 15	⊢
	: , : , :
10	instantiation	16, 341, 338, 274, 17, 275, 301, 272, 154, 18*, 19*	⊢
	: , : , : , : , : , :
11	instantiation	20, 335, 301	⊢
	: , :
12	instantiation	21, 338, 22, 23, 24	⊢
	: , : , : , :
13	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
14	instantiation	28, 338, 274, 25, 275, 320, 26, 27	⊢
	: , : , : , : , : , :
15	instantiation	28, 341, 320, 29, 30	⊢
	: , : , : , : , : , :
16	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
17	instantiation	290	⊢
	: , :
18	instantiation	31, 301	⊢
	:
19	instantiation	216, 32, 33	⊢
	: , : , :
20	theorem		⊢
	proveit.numbers.exponentiation.exp_nat_pos_expansion
21	theorem		⊢
	proveit.core_expr_types.operations.operands_substitution_via_tuple
22	instantiation	34, 338	⊢
	: , :
23	instantiation	290	⊢
	: , :
24	instantiation	35	⊢
	:
25	instantiation	290	⊢
	: , :
26	instantiation	316, 41	⊢
	:
27	instantiation	39, 38, 36, 37	⊢
	: , :
28	theorem		⊢
	proveit.numbers.addition.weak_bound_via_term_bound
29	instantiation	316, 38	⊢
	:
30	instantiation	39, 40, 41, 42	⊢
	: , :
31	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
32	instantiation	216, 43, 44	⊢
	: , : , :
33	instantiation	259, 45, 46	⊢
	: , : , :
34	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
35	theorem		⊢
	proveit.numbers.numerals.decimals.reduce_2_repeats
36	instantiation	101, 320, 47, 48	⊢
	: , :
37	instantiation	57, 58, 87, 49, 50	⊢
	: , : , :
38	instantiation	101, 320, 51, 52	⊢
	: , :
39	theorem		⊢
	proveit.numbers.negation.negated_weak_bound
40	instantiation	101, 320, 53, 54	⊢
	: , :
41	instantiation	101, 320, 55, 56	⊢
	: , :
42	instantiation	57, 58, 95, 59, 60	⊢
	: , : , :
43	instantiation	61, 272, 288, 62, 63	⊢
	: , : , : , : , :
44	instantiation	257, 64	⊢
	: , : , :
45	instantiation	257, 65	⊢
	: , : , :
46	instantiation	111, 66	⊢
	:
47	instantiation	74, 71, 68	⊢
	: , :
48	instantiation	245, 67	⊢
	:
49	instantiation	339, 326, 92	⊢
	: , : , :
50	instantiation	80, 71, 68, 72, 69, 70	⊢
	: , : , :
51	instantiation	74, 71, 72	⊢
	: , :
52	instantiation	75, 73	⊢
	:
53	instantiation	74, 311, 168	⊢
	: , :
54	instantiation	75, 76	⊢
	:
55	instantiation	339, 302, 95	⊢
	: , : , :
56	instantiation	245, 77	⊢
	:
57	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
58	instantiation	339, 78, 79	⊢
	: , : , :
59	instantiation	339, 326, 94	⊢
	: , : , :
60	instantiation	80, 311, 114, 168, 106, 81	⊢
	: , : , :
61	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
62	instantiation	339, 298, 82	⊢
	: , : , :
63	instantiation	339, 298, 83	⊢
	: , : , :
64	instantiation	259, 84, 85	⊢
	: , : , :
65	instantiation	100, 272	⊢
	:
66	instantiation	339, 310, 86	⊢
	: , : , :
67	instantiation	339, 255, 87	⊢
	: , : , :
68	instantiation	91, 114, 338	⊢
	: , :
69	instantiation	88, 311, 114, 168, 89, 170	⊢
	: , : , :
70	instantiation	97, 121	⊢
	:
71	instantiation	339, 329, 90	⊢
	: , : , :
72	instantiation	91, 168, 338	⊢
	: , :
73	instantiation	339, 93, 92	⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
75	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_if_in_rational_nonzero
76	instantiation	339, 93, 94	⊢
	: , : , :
77	instantiation	339, 255, 95	⊢
	: , : , :
78	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
79	instantiation	339, 96, 341	⊢
	: , : , :
80	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
81	instantiation	97, 338	⊢
	:
82	instantiation	339, 308, 98	⊢
	: , : , :
83	instantiation	339, 255, 296	⊢
	: , : , :
84	instantiation	257, 99	⊢
	: , : , :
85	instantiation	100, 301	⊢
	:
86	instantiation	101, 320, 306, 269	⊢
	: , :
87	instantiation	279, 102, 103	⊢
	: , :
88	theorem		⊢
	proveit.numbers.exponentiation.exp_pos_lesseq
89	instantiation	104, 105, 106	⊢
	: , :
90	instantiation	339, 336, 107	⊢
	: , : , :
91	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
92	instantiation	109, 112, 108	⊢
	: , :
93	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
94	instantiation	109, 327, 123	⊢
	: , :
95	instantiation	279, 314, 135	⊢
	: , :
96	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
97	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
98	instantiation	339, 322, 110	⊢
	: , : , :
99	instantiation	111, 301	⊢
	:
100	theorem		⊢
	proveit.numbers.division.frac_one_denom
101	theorem		⊢
	proveit.numbers.division.div_real_closure
102	instantiation	339, 326, 112	⊢
	: , : , :
103	instantiation	113, 114, 115	⊢
	:
104	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
105	instantiation	116, 117	⊢
	:
106	instantiation	146, 304, 118, 215, 119, 120*	⊢
	: , : , :
107	instantiation	339, 340, 121	⊢
	: , : , :
108	instantiation	122, 123, 332	⊢
	: , :
109	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
110	instantiation	339, 331, 333	⊢
	: , : , :
111	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
112	instantiation	339, 334, 124	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.exponentiation.sqrd_pos_closure
114	instantiation	159, 320, 165	⊢
	: , :
115	instantiation	245, 125	⊢
	:
116	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
117	instantiation	339, 126, 135	⊢
	: , : , :
118	instantiation	339, 302, 207	⊢
	: , : , :
119	instantiation	127, 311, 193, 128, 282, 129, 130*	⊢
	: , : , :
120	instantiation	259, 131, 132	⊢
	: , : , :
121	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
122	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_pos_closure
123	instantiation	133, 177, 134	⊢
	:
124	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
125	instantiation	339, 255, 135	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonneg
127	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
128	instantiation	159, 149, 147	⊢
	: , :
129	instantiation	136, 137, 138	⊢
	: , : , :
130	instantiation	139, 314, 207, 251	⊢
	: , :
131	instantiation	201, 274, 338, 341, 275, 140, 301, 154, 294	⊢
	: , : , : , : , : , :
132	instantiation	259, 141, 142	⊢
	: , : , :
133	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.pos_rational_is_rational_pos
134	instantiation	143, 144	⊢
	: , :
135	instantiation	262, 313, 219	⊢
	: , :
136	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
137	instantiation	145, 193	⊢
	:
138	instantiation	146, 147, 148, 149, 150, 151*	⊢
	: , : , :
139	theorem		⊢
	proveit.numbers.exponentiation.exponent_log_with_same_base
140	instantiation	290	⊢
	: , :
141	instantiation	152, 341, 274, 275, 301, 154, 294	⊢
	: , : , : , : , : , : , :
142	instantiation	203, 274, 338, 341, 275, 153, 301, 294, 154, 217*	⊢
	: , : , : , : , : , :
143	theorem		⊢
	proveit.numbers.addition.subtraction.pos_difference
144	instantiation	155, 304, 311, 156, 157, 217*, 158*	⊢
	: , : , :
145	theorem		⊢
	proveit.numbers.rounding.ceil_x_ge_x
146	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
147	instantiation	316, 221	⊢
	:
148	instantiation	159, 221, 160	⊢
	: , :
149	instantiation	229, 230, 265	⊢
	: , : , :
150	axiom		⊢
	proveit.physics.quantum.QPE._t_req
151	instantiation	161, 162, 163, 164	⊢
	: , : , : , :
152	theorem		⊢
	proveit.numbers.addition.leftward_commutation
153	instantiation	290	⊢
	: , :
154	instantiation	339, 310, 165	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
156	instantiation	339, 329, 166	⊢
	: , : , :
157	instantiation	167, 311, 168, 169, 170	⊢
	: , : , :
158	instantiation	259, 171, 172	⊢
	: , : , :
159	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
160	instantiation	339, 329, 173	⊢
	: , : , :
161	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
162	instantiation	259, 174, 175	⊢
	: , : , :
163	instantiation	212	⊢
	:
164	instantiation	176, 194	⊢
	: , :
165	instantiation	339, 302, 219	⊢
	: , : , :
166	instantiation	186, 177, 324	⊢
	: , :
167	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
168	instantiation	339, 329, 177	⊢
	: , : , :
169	theorem		⊢
	proveit.physics.quantum.QPE._e_value_ge_two
170	instantiation	178, 335	⊢
	:
171	instantiation	257, 179	⊢
	: , : , :
172	instantiation	259, 180, 181	⊢
	: , : , :
173	instantiation	339, 336, 182	⊢
	: , : , :
174	instantiation	257, 183	⊢
	: , : , :
175	instantiation	259, 184, 185	⊢
	: , : , :
176	theorem		⊢
	proveit.logic.equality.equals_reversal
177	instantiation	186, 224, 187	⊢
	: , :
178	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
179	instantiation	259, 188, 189	⊢
	: , : , :
180	instantiation	201, 274, 338, 341, 275, 190, 205, 272, 294	⊢
	: , : , : , : , : , :
181	instantiation	191, 272, 205, 192	⊢
	: , : , :
182	instantiation	240, 193	⊢
	:
183	instantiation	257, 194	⊢
	: , : , :
184	instantiation	201, 274, 338, 341, 275, 195, 210, 198, 196	⊢
	: , : , : , : , : , :
185	instantiation	197, 210, 198, 199	⊢
	: , : , :
186	theorem		⊢
	proveit.numbers.addition.add_rational_closure_bin
187	instantiation	339, 336, 200	⊢
	: , : , :
188	instantiation	201, 274, 338, 341, 275, 202, 205, 294, 301	⊢
	: , : , : , : , : , :
189	instantiation	203, 341, 338, 274, 204, 275, 205, 294, 301, 206*	⊢
	: , : , : , : , : , :
190	instantiation	290	⊢
	: , :
191	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
192	instantiation	212	⊢
	:
193	instantiation	249, 314, 207, 251	⊢
	: , :
194	instantiation	257, 208	⊢
	: , : , :
195	instantiation	290	⊢
	: , :
196	instantiation	209, 210	⊢
	:
197	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
198	instantiation	339, 310, 211	⊢
	: , : , :
199	instantiation	212	⊢
	:
200	instantiation	339, 213, 214	⊢
	: , : , :
201	theorem		⊢
	proveit.numbers.addition.disassociation
202	instantiation	290	⊢
	: , :
203	theorem		⊢
	proveit.numbers.addition.association
204	instantiation	290	⊢
	: , :
205	instantiation	339, 310, 215	⊢
	: , : , :
206	instantiation	216, 217, 218	⊢
	: , : , :
207	instantiation	262, 314, 219	⊢
	: , :
208	instantiation	257, 220	⊢
	: , : , :
209	theorem		⊢
	proveit.numbers.negation.complex_closure
210	instantiation	339, 310, 221	⊢
	: , : , :
211	instantiation	339, 329, 222	⊢
	: , : , :
212	axiom		⊢
	proveit.logic.equality.equals_reflexivity
213	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
214	instantiation	223, 333	⊢
	:
215	instantiation	339, 329, 224	⊢
	: , : , :
216	theorem		⊢
	proveit.logic.equality.sub_right_side_into
217	instantiation	225, 272, 301, 226	⊢
	: , : , :
218	instantiation	227, 301, 294	⊢
	: , :
219	instantiation	312, 313, 256, 236	⊢
	: , :
220	instantiation	257, 228	⊢
	: , : , :
221	instantiation	229, 230, 284	⊢
	: , : , :
222	instantiation	339, 336, 231	⊢
	: , : , :
223	theorem		⊢
	proveit.numbers.negation.int_neg_closure
224	instantiation	339, 232, 233	⊢
	: , : , :
225	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
226	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
227	theorem		⊢
	proveit.numbers.addition.commutation
228	instantiation	234, 272, 235, 236, 237*	⊢
	: , :
229	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
230	instantiation	238, 239	⊢
	: , :
231	instantiation	240, 241	⊢
	:
232	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
233	instantiation	242, 309, 243	⊢
	: , :
234	theorem		⊢
	proveit.numbers.division.div_as_mult
235	instantiation	339, 310, 244	⊢
	: , : , :
236	instantiation	245, 246	⊢
	:
237	instantiation	259, 247, 248	⊢
	: , : , :
238	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
239	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
240	axiom		⊢
	proveit.numbers.rounding.ceil_is_an_int
241	instantiation	249, 314, 250, 251	⊢
	: , :
242	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
243	instantiation	252, 253, 254	⊢
	: , :
244	instantiation	339, 302, 256	⊢
	: , : , :
245	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
246	instantiation	339, 255, 256	⊢
	: , : , :
247	instantiation	257, 258	⊢
	: , : , :
248	instantiation	259, 260, 261	⊢
	: , : , :
249	theorem		⊢
	proveit.numbers.logarithms.log_real_pos_real_closure
250	instantiation	262, 314, 263	⊢
	: , :
251	instantiation	285, 264	⊢
	: , :
252	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
253	instantiation	339, 283, 265	⊢
	: , : , :
254	instantiation	266, 267	⊢
	:
255	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
256	instantiation	279, 314, 296	⊢
	: , :
257	axiom		⊢
	proveit.logic.equality.substitution
258	instantiation	268, 301, 293, 304, 315, 269, 270*	⊢
	: , : , :
259	axiom		⊢
	proveit.logic.equality.equals_transitivity
260	instantiation	271, 341, 338, 274, 276, 275, 272, 277, 278	⊢
	: , : , : , : , : , :
261	instantiation	273, 274, 338, 275, 276, 277, 278	⊢
	: , : , : , :
262	theorem		⊢
	proveit.numbers.addition.add_real_pos_closure_bin
263	instantiation	279, 303, 280	⊢
	: , :
264	instantiation	281, 341, 338, 282	⊢
	: , :
265	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
266	theorem		⊢
	proveit.numbers.negation.int_closure
267	instantiation	339, 283, 284	⊢
	: , : , :
268	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
269	instantiation	285, 286	⊢
	: , :
270	instantiation	287, 288, 333, 289*	⊢
	: , :
271	theorem		⊢
	proveit.numbers.multiplication.disassociation
272	instantiation	339, 310, 320	⊢
	: , : , :
273	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
274	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
275	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
276	instantiation	290	⊢
	: , :
277	instantiation	339, 310, 291	⊢
	: , : , :
278	instantiation	292, 293, 294	⊢
	: , :
279	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
280	instantiation	295, 296, 304	⊢
	: , :
281	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
282	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
283	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
284	axiom		⊢
	proveit.physics.quantum.QPE._n_in_natural_pos
285	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
286	instantiation	297, 319, 306, 307	⊢
	: , :
287	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
288	instantiation	339, 298, 299	⊢
	: , : , :
289	instantiation	300, 301	⊢
	:
290	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
291	instantiation	339, 302, 303	⊢
	: , : , :
292	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
293	instantiation	339, 310, 306	⊢
	: , : , :
294	instantiation	339, 310, 304	⊢
	: , : , :
295	theorem		⊢
	proveit.numbers.exponentiation.exp_real_pos_closure
296	instantiation	305, 306, 307	⊢
	:
297	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq
298	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
299	instantiation	339, 308, 309	⊢
	: , : , :
300	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
301	instantiation	339, 310, 311	⊢
	: , : , :
302	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
303	instantiation	312, 313, 314, 315	⊢
	: , :
304	instantiation	316, 320	⊢
	:
305	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
306	instantiation	317, 319, 320, 321	⊢
	: , : , :
307	instantiation	318, 319, 320, 321	⊢
	: , : , :
308	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
309	instantiation	339, 322, 323	⊢
	: , : , :
310	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
311	instantiation	339, 329, 324	⊢
	: , : , :
312	theorem		⊢
	proveit.numbers.division.div_real_pos_closure
313	instantiation	339, 326, 325	⊢
	: , : , :
314	instantiation	339, 326, 327	⊢
	: , : , :
315	instantiation	328, 335	⊢
	:
316	theorem		⊢
	proveit.numbers.negation.real_closure
317	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
318	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
319	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
320	instantiation	339, 329, 330	⊢
	: , : , :
321	axiom		⊢
	proveit.physics.quantum.QPE._eps_in_interval
322	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
323	instantiation	339, 331, 335	⊢
	: , : , :
324	instantiation	339, 336, 332	⊢
	: , : , :
325	instantiation	339, 334, 333	⊢
	: , : , :
326	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
327	instantiation	339, 334, 335	⊢
	: , : , :
328	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
329	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
330	instantiation	339, 336, 337	⊢
	: , : , :
331	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
332	instantiation	339, 340, 338	⊢
	: , : , :
333	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
334	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
335	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
336	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
337	instantiation	339, 340, 341	⊢
	: , : , :
338	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
339	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
340	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
341	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements