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