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