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