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