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_right_side_into
2	instantiation	97, 4, 34, 5, 6, 7*	⊢
	: , : , :
3	instantiation	195, 8	⊢
	: , : , :
4	instantiation	148, 9, 62	⊢
	: , :
5	instantiation	129, 62, 9, 63, 10	⊢
	: , : , :
6	instantiation	129, 62, 282, 63, 11, 12*	⊢
	: , : , :
7	instantiation	107, 13, 14, 15	⊢
	: , : , : , :
8	instantiation	195, 16	⊢
	: , : , :
9	instantiation	69, 235, 17	⊢
	: , :
10	instantiation	18, 235, 98, 58, 262, 19	⊢
	: , : , :
11	instantiation	20, 21	⊢
	:
12	instantiation	22, 243, 23	⊢
	: , :
13	instantiation	162, 163, 261, 290, 164, 25, 56, 39, 24	⊢
	: , : , : , : , : , :
14	instantiation	162, 261, 163, 25, 164, 56, 39	⊢
	: , : , : , : , : , :
15	instantiation	107, 26, 27, 28	⊢
	: , : , : , :
16	instantiation	29, 39, 140	⊢
	: , :
17	instantiation	74, 30, 31	⊢
	:
18	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
19	instantiation	158, 150, 188, 149, 32	⊢
	: , : , :
20	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
21	instantiation	33, 261, 70	⊢
	: , :
22	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
23	instantiation	190	⊢
	:
24	instantiation	288, 250, 34	⊢
	: , : , :
25	instantiation	241	⊢
	: , :
26	instantiation	77, 290, 56, 39	⊢
	: , : , : , : , : , : , :
27	instantiation	78, 163, 261, 164, 35, 37, 56, 39, 36*	⊢
	: , : , : , : , : , :
28	instantiation	78, 290, 261, 163, 37, 164, 38, 39, 40*	⊢
	: , : , : , : , : , :
29	theorem		⊢
	proveit.numbers.addition.commutation
30	instantiation	81, 82, 41	⊢
	: , :
31	instantiation	84, 91	⊢
	: , :
32	instantiation	42, 235, 211, 90	⊢
	: , :
33	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
34	instantiation	148, 63, 62	⊢
	: , :
35	instantiation	241	⊢
	: , :
36	instantiation	43, 44, 45*	⊢
	: , :
37	instantiation	241	⊢
	: , :
38	instantiation	46, 222, 47	⊢
	: , :
39	instantiation	135, 243	⊢
	:
40	instantiation	48, 243, 222, 113	⊢
	: , : , :
41	instantiation	288, 88, 49	⊢
	: , : , :
42	theorem		⊢
	proveit.numbers.negation.negated_weak_bound
43	theorem		⊢
	proveit.logic.equality.equals_reversal
44	instantiation	50, 163, 261, 290, 164, 51, 243, 56, 52*	⊢
	: , : , : , : , : , :
45	instantiation	216, 53, 54	⊢
	: , : , :
46	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
47	instantiation	288, 250, 55	⊢
	: , : , :
48	theorem		⊢
	proveit.numbers.addition.subtraction.negated_add
49	instantiation	92, 227	⊢
	:
50	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
51	instantiation	241	⊢
	: , :
52	instantiation	209, 56	⊢
	:
53	instantiation	195, 113	⊢
	: , : , :
54	instantiation	57, 222, 282, 58, 59, 60*, 61*	⊢
	: , : , :
55	instantiation	148, 62, 150	⊢
	: , :
56	instantiation	288, 250, 63	⊢
	: , : , :
57	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
58	instantiation	288, 284, 64	⊢
	: , : , :
59	instantiation	65, 278	⊢
	:
60	instantiation	66, 222	⊢
	:
61	instantiation	216, 67, 68	⊢
	: , : , :
62	instantiation	210, 282	⊢
	:
63	instantiation	69, 235, 70	⊢
	: , :
64	instantiation	288, 286, 75	⊢
	: , : , :
65	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
66	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
67	instantiation	162, 290, 261, 163, 71, 164, 243, 140, 121	⊢
	: , : , : , : , : , :
68	instantiation	216, 72, 73	⊢
	: , : , :
69	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
70	instantiation	74, 75, 76	⊢
	:
71	instantiation	241	⊢
	: , :
72	instantiation	77, 290, 163, 164, 243, 140, 121	⊢
	: , : , : , : , : , : , :
73	instantiation	78, 163, 261, 290, 164, 79, 243, 121, 140, 80*	⊢
	: , : , : , : , : , :
74	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
75	instantiation	81, 82, 83	⊢
	: , :
76	instantiation	84, 85	⊢
	: , :
77	theorem		⊢
	proveit.numbers.addition.leftward_commutation
78	theorem		⊢
	proveit.numbers.addition.association
79	instantiation	241	⊢
	: , :
80	instantiation	86, 243, 222, 113	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
82	instantiation	288, 87, 171	⊢
	: , : , :
83	instantiation	288, 88, 89	⊢
	: , : , :
84	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
85	instantiation	114, 90, 91	⊢
	: , : , :
86	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
87	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
88	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
89	instantiation	92, 278	⊢
	:
90	axiom		⊢
	proveit.physics.quantum.QPE._n_ge_two
91	instantiation	129, 133, 235, 93, 94, 95*, 96*	⊢
	: , : , :
92	theorem		⊢
	proveit.numbers.negation.int_neg_closure
93	instantiation	148, 98, 235	⊢
	: , :
94	instantiation	97, 235, 98, 99, 205	⊢
	: , : , :
95	instantiation	216, 100, 101	⊢
	: , : , :
96	instantiation	216, 102, 103	⊢
	: , : , :
97	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right
98	instantiation	148, 150, 188	⊢
	: , :
99	instantiation	114, 104, 105	⊢
	: , : , :
100	instantiation	162, 290, 261, 163, 120, 164, 222, 168, 121	⊢
	: , : , : , : , : , :
101	instantiation	167, 222, 168, 138	⊢
	: , : , :
102	instantiation	195, 106	⊢
	: , : , :
103	instantiation	107, 108, 109, 110	⊢
	: , : , : , :
104	instantiation	111, 287, 127, 112, 113*	⊢
	: , :
105	instantiation	114, 115, 116	⊢
	: , : , :
106	instantiation	162, 163, 261, 290, 164, 137, 140, 166, 222	⊢
	: , : , : , : , : , :
107	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
108	instantiation	162, 163, 118, 290, 164, 119, 140, 166, 222, 117	⊢
	: , : , : , : , : , :
109	instantiation	162, 118, 261, 163, 119, 120, 164, 140, 166, 222, 168, 121	⊢
	: , : , : , : , : , :
110	instantiation	216, 122, 123	⊢
	: , : , :
111	theorem		⊢
	proveit.numbers.rounding.ceil_of_real_above_int
112	instantiation	124, 270, 144, 125	⊢
	: , :
113	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
114	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
115	instantiation	126, 127, 239, 128	⊢
	: , :
116	instantiation	129, 188, 130, 150, 131, 132*	⊢
	: , : , :
117	instantiation	288, 250, 133	⊢
	: , : , :
118	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
119	instantiation	134	⊢
	: , : , :
120	instantiation	241	⊢
	: , :
121	instantiation	135, 222	⊢
	:
122	instantiation	136, 261, 290, 163, 137, 164, 140, 166, 222, 168, 138	⊢
	: , : , : , : , : , : , : , :
123	instantiation	139, 168, 140, 170	⊢
	: , : , :
124	theorem		⊢
	proveit.numbers.logarithms.log_base_large_a_greater_one
125	instantiation	141, 262, 142	⊢
	: , :
126	theorem		⊢
	proveit.numbers.rounding.ceil_increasing_less_eq
127	instantiation	245, 270, 144, 247	⊢
	: , :
128	instantiation	143, 270, 144, 246, 145, 262	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
130	instantiation	148, 211, 189	⊢
	: , :
131	axiom		⊢
	proveit.physics.quantum.QPE._t_req
132	instantiation	216, 146, 147	⊢
	: , : , :
133	instantiation	148, 211, 149	⊢
	: , :
134	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
135	theorem		⊢
	proveit.numbers.negation.complex_closure
136	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
137	instantiation	241	⊢
	: , :
138	instantiation	190	⊢
	:
139	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
140	instantiation	288, 250, 150	⊢
	: , : , :
141	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
142	instantiation	151, 235, 152, 153, 154, 155*, 156*	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.logarithms.log_increasing_less_eq
144	instantiation	288, 272, 157	⊢
	: , : , :
145	instantiation	158, 235, 229, 159, 160, 161*	⊢
	: , : , :
146	instantiation	162, 163, 261, 290, 164, 165, 168, 169, 166	⊢
	: , : , : , : , : , :
147	instantiation	167, 168, 169, 170	⊢
	: , : , :
148	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
149	instantiation	210, 235	⊢
	:
150	instantiation	225, 226, 171	⊢
	: , : , :
151	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
152	instantiation	172, 229, 281	⊢
	: , :
153	instantiation	288, 284, 173	⊢
	: , : , :
154	instantiation	174, 229, 281, 282, 175, 176	⊢
	: , : , :
155	instantiation	216, 177, 178	⊢
	: , : , :
156	instantiation	216, 179, 180	⊢
	: , : , :
157	instantiation	256, 181, 273	⊢
	: , :
158	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
159	instantiation	288, 182, 253	⊢
	: , : , :
160	instantiation	183, 184, 268, 270, 185	⊢
	: , : , :
161	instantiation	197, 251, 287, 198*, 186*, 187*	⊢
	: , : , : , :
162	theorem		⊢
	proveit.numbers.addition.disassociation
163	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
164	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
165	instantiation	241	⊢
	: , :
166	instantiation	288, 250, 188	⊢
	: , : , :
167	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
168	instantiation	288, 250, 211	⊢
	: , : , :
169	instantiation	288, 250, 189	⊢
	: , : , :
170	instantiation	190	⊢
	:
171	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
172	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
173	instantiation	191, 240, 285	⊢
	: , :
174	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
175	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
176	instantiation	192, 249	⊢
	:
177	instantiation	195, 193	⊢
	: , : , :
178	instantiation	194, 222	⊢
	:
179	instantiation	195, 196	⊢
	: , : , :
180	instantiation	197, 287, 251, 198*, 199*, 206*	⊢
	: , : , : , :
181	instantiation	288, 277, 200	⊢
	: , : , :
182	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
183	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
184	instantiation	288, 201, 202	⊢
	: , : , :
185	instantiation	203, 235, 275, 282, 204, 205, 206*	⊢
	: , : , :
186	instantiation	216, 207, 208	⊢
	: , : , :
187	instantiation	209, 222	⊢
	:
188	instantiation	210, 211	⊢
	:
189	instantiation	288, 284, 212	⊢
	: , : , :
190	axiom		⊢
	proveit.logic.equality.equals_reflexivity
191	theorem		⊢
	proveit.numbers.multiplication.mult_rational_closure_bin
192	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
193	instantiation	213, 214	⊢
	:
194	theorem		⊢
	proveit.numbers.addition.elim_zero_left
195	axiom		⊢
	proveit.logic.equality.substitution
196	instantiation	242, 214	⊢
	:
197	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
198	instantiation	215, 222	⊢
	:
199	instantiation	216, 217, 218	⊢
	: , : , :
200	theorem		⊢
	proveit.numbers.numerals.decimals.posnat5
201	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
202	instantiation	288, 219, 290	⊢
	: , : , :
203	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
204	instantiation	220, 281, 282, 283	⊢
	: , : , :
205	instantiation	221, 261	⊢
	:
206	instantiation	242, 222	⊢
	:
207	instantiation	230, 261, 223, 224, 234, 233	⊢
	: , : , : , :
208	theorem		⊢
	proveit.numbers.numerals.decimals.add_4_1
209	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
210	theorem		⊢
	proveit.numbers.negation.real_closure
211	instantiation	225, 226, 227	⊢
	: , : , :
212	instantiation	288, 286, 228	⊢
	: , : , :
213	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
214	instantiation	288, 250, 229	⊢
	: , : , :
215	theorem		⊢
	proveit.numbers.division.frac_one_denom
216	axiom		⊢
	proveit.logic.equality.equals_transitivity
217	instantiation	230, 261, 231, 232, 233, 234	⊢
	: , : , : , :
218	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_4
219	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
220	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
221	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
222	instantiation	288, 250, 235	⊢
	: , : , :
223	instantiation	241	⊢
	: , :
224	instantiation	241	⊢
	: , :
225	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
226	instantiation	236, 237	⊢
	: , :
227	axiom		⊢
	proveit.physics.quantum.QPE._n_in_natural_pos
228	instantiation	238, 239	⊢
	:
229	instantiation	288, 284, 240	⊢
	: , : , :
230	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
231	instantiation	241	⊢
	: , :
232	instantiation	241	⊢
	: , :
233	instantiation	242, 243	⊢
	:
234	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
235	instantiation	288, 284, 244	⊢
	: , : , :
236	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
237	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
238	axiom		⊢
	proveit.numbers.rounding.ceil_is_an_int
239	instantiation	245, 270, 246, 247	⊢
	: , :
240	instantiation	288, 248, 249	⊢
	: , : , :
241	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
242	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
243	instantiation	288, 250, 282	⊢
	: , : , :
244	instantiation	288, 286, 251	⊢
	: , : , :
245	theorem		⊢
	proveit.numbers.logarithms.log_real_pos_real_closure
246	instantiation	252, 270, 253	⊢
	: , :
247	instantiation	254, 255	⊢
	: , :
248	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
249	instantiation	256, 263, 273	⊢
	: , :
250	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
251	instantiation	288, 289, 261	⊢
	: , : , :
252	theorem		⊢
	proveit.numbers.addition.add_real_pos_closure_bin
253	instantiation	257, 258, 268, 259	⊢
	: , :
254	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
255	instantiation	260, 290, 261, 262	⊢
	: , :
256	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
257	theorem		⊢
	proveit.numbers.division.div_real_pos_closure
258	instantiation	288, 272, 263	⊢
	: , : , :
259	instantiation	264, 265	⊢
	:
260	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
261	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
262	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
263	instantiation	288, 277, 266	⊢
	: , : , :
264	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
265	instantiation	288, 267, 268	⊢
	: , : , :
266	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
267	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
268	instantiation	269, 270, 271	⊢
	: , :
269	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
270	instantiation	288, 272, 273	⊢
	: , : , :
271	instantiation	274, 275, 276	⊢
	:
272	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
273	instantiation	288, 277, 278	⊢
	: , : , :
274	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
275	instantiation	279, 281, 282, 283	⊢
	: , : , :
276	instantiation	280, 281, 282, 283	⊢
	: , : , :
277	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
278	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
279	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
280	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
281	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
282	instantiation	288, 284, 285	⊢
	: , : , :
283	axiom		⊢
	proveit.physics.quantum.QPE._eps_in_interval
284	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
285	instantiation	288, 286, 287	⊢
	: , : , :
286	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
287	instantiation	288, 289, 290	⊢
	: , : , :
288	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
289	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
290	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements