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