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