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