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