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