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