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