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	⊢
	: , : , :
1	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
2	reference	27	⊢
3	reference	170	⊢
4	instantiation	5, 6	⊢
	:
5	theorem		⊢
	proveit.trigonometry.sine_pos_interval
6	instantiation	7, 27, 95, 8, 9	⊢
	: , : , :
7	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
8	instantiation	206, 122, 13	⊢
	: , : , :
9	instantiation	10, 11, 12	⊢
	: , :
10	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
11	instantiation	82, 13	⊢
	:
12	instantiation	14, 15, 16	⊢
	: , : , :
13	instantiation	17, 121, 123	⊢
	: , :
14	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
15	instantiation	55, 18, 36	⊢
	: , : , :
16	instantiation	66, 64, 19, 20, 21*, 22*	⊢
	: , : , :
17	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
18	instantiation	23, 24, 25	⊢
	: , : , :
19	instantiation	83, 84, 27	⊢
	: , :
20	instantiation	26, 84, 27, 95, 58, 28	⊢
	: , : , :
21	instantiation	156, 29, 30	⊢
	: , : , :
22	instantiation	31, 32, 33*	⊢
	: , :
23	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
24	instantiation	34, 35, 36	⊢
	: , : , :
25	instantiation	37, 95, 38, 151, 39, 40, 41*, 42*	⊢
	: , : , :
26	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
27	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
28	instantiation	43, 133	⊢
	:
29	instantiation	97, 44	⊢
	: , : , :
30	instantiation	45, 46	⊢
	:
31	theorem		⊢
	proveit.logic.equality.equals_reversal
32	instantiation	47, 114, 208, 201, 115, 48, 63, 72	⊢
	: , : , : , : , : , :
33	instantiation	156, 49, 50	⊢
	: , : , :
34	theorem		⊢
	proveit.logic.equality.sub_left_side_into
35	instantiation	51, 201, 121, 123, 52, 53*	⊢
	: , : , : , : , : , :
36	instantiation	97, 54	⊢
	: , : , :
37	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
38	instantiation	83, 146, 96	⊢
	: , :
39	instantiation	55, 56, 57	⊢
	: , : , :
40	instantiation	130, 58	⊢
	: , :
41	instantiation	59, 201, 208, 114, 60, 115, 72, 119, 73	⊢
	: , : , : , : , : , :
42	instantiation	61, 72, 63	⊢
	: , :
43	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
44	instantiation	62, 63	⊢
	:
45	theorem		⊢
	proveit.numbers.addition.elim_zero_left
46	instantiation	206, 198, 64	⊢
	: , : , :
47	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
48	instantiation	189	⊢
	: , :
49	instantiation	97, 65	⊢
	: , : , :
50	instantiation	190, 72	⊢
	:
51	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
52	instantiation	66, 145, 199, 67, 68, 69*, 70*	⊢
	: , : , :
53	instantiation	71, 201, 72, 73	⊢
	: , : , : , :
54	instantiation	156, 74, 75	⊢
	: , : , :
55	theorem		⊢
	proveit.logic.equality.sub_right_side_into
56	instantiation	76, 77, 78	⊢
	: , :
57	instantiation	79, 188, 80, 119, 167, 81*	⊢
	: , :
58	instantiation	82, 121	⊢
	:
59	theorem		⊢
	proveit.numbers.multiplication.disassociation
60	instantiation	189	⊢
	: , :
61	theorem		⊢
	proveit.numbers.multiplication.commutation
62	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
63	instantiation	206, 198, 151	⊢
	: , : , :
64	instantiation	83, 84, 95	⊢
	: , :
65	instantiation	85, 197, 205, 86*	⊢
	: , : , : , :
66	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
67	instantiation	206, 202, 87	⊢
	: , : , :
68	instantiation	88, 199, 146, 170, 89, 90	⊢
	: , : , :
69	instantiation	91, 125, 192, 92	⊢
	: , : , :
70	instantiation	156, 93, 94	⊢
	: , : , :
71	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
72	instantiation	206, 198, 95	⊢
	: , : , :
73	instantiation	206, 198, 96	⊢
	: , : , :
74	instantiation	97, 98	⊢
	: , : , :
75	instantiation	99, 167	⊢
	:
76	theorem		⊢
	proveit.numbers.absolute_value.weak_upper_bound
77	instantiation	100, 128, 151, 129	⊢
	: , : , :
78	instantiation	130, 101	⊢
	: , :
79	theorem		⊢
	proveit.numbers.absolute_value.abs_prod
80	instantiation	189	⊢
	: , :
81	instantiation	102, 103	⊢
	:
82	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
83	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
84	instantiation	206, 202, 104	⊢
	: , : , :
85	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
86	instantiation	156, 105, 106	⊢
	: , : , :
87	instantiation	206, 204, 107	⊢
	: , : , :
88	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
89	instantiation	108, 199, 170, 109, 110, 111, 112*	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
91	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
92	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
93	instantiation	113, 114, 208, 201, 115, 116, 119, 125, 117	⊢
	: , : , : , : , : , :
94	instantiation	118, 125, 119, 120	⊢
	: , : , :
95	instantiation	206, 122, 121	⊢
	: , : , :
96	instantiation	206, 122, 123	⊢
	: , : , :
97	axiom		⊢
	proveit.logic.equality.substitution
98	instantiation	124, 125, 167, 126*	⊢
	: , :
99	theorem		⊢
	proveit.numbers.absolute_value.abs_even
100	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
101	instantiation	127, 128, 151, 129	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
103	instantiation	130, 131	⊢
	: , :
104	instantiation	206, 132, 133	⊢
	: , : , :
105	instantiation	174, 208, 134, 135, 136, 137	⊢
	: , : , : , :
106	instantiation	138, 139, 140	⊢
	:
107	instantiation	206, 207, 141	⊢
	: , : , :
108	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
109	instantiation	164, 165, 143	⊢
	: , : , :
110	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
111	instantiation	142, 143	⊢
	:
112	instantiation	144, 192	⊢
	:
113	theorem		⊢
	proveit.numbers.addition.disassociation
114	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
115	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
116	instantiation	189	⊢
	: , :
117	instantiation	206, 198, 145	⊢
	: , : , :
118	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
119	instantiation	206, 198, 146	⊢
	: , : , :
120	instantiation	147	⊢
	:
121	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
122	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
123	instantiation	148, 149	⊢
	:
124	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
125	instantiation	206, 198, 170	⊢
	: , : , :
126	instantiation	190, 167	⊢
	:
127	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
128	instantiation	150, 151	⊢
	:
129	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
130	theorem		⊢
	proveit.numbers.ordering.relax_less
131	instantiation	152, 181	⊢
	:
132	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
133	instantiation	153, 154, 155	⊢
	: , :
134	instantiation	189	⊢
	: , :
135	instantiation	189	⊢
	: , :
136	instantiation	156, 157, 158	⊢
	: , : , :
137	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
138	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
139	instantiation	206, 198, 159	⊢
	: , : , :
140	instantiation	187, 160	⊢
	:
141	instantiation	161, 162, 201	⊢
	: , :
142	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
143	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
144	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
145	instantiation	206, 202, 163	⊢
	: , : , :
146	instantiation	164, 165, 181	⊢
	: , : , :
147	axiom		⊢
	proveit.logic.equality.equals_reflexivity
148	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
149	instantiation	166, 167, 168	⊢
	:
150	theorem		⊢
	proveit.numbers.negation.real_closure
151	instantiation	169, 170, 199, 171	⊢
	: , :
152	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
153	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
154	instantiation	206, 173, 172	⊢
	: , : , :
155	instantiation	206, 173, 188	⊢
	: , : , :
156	axiom		⊢
	proveit.logic.equality.equals_transitivity
157	instantiation	174, 208, 175, 176, 177, 178	⊢
	: , : , : , :
158	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
159	instantiation	206, 202, 179	⊢
	: , : , :
160	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
161	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
162	instantiation	206, 180, 181	⊢
	: , : , :
163	instantiation	206, 204, 182	⊢
	: , : , :
164	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
165	instantiation	183, 184	⊢
	: , :
166	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
167	instantiation	206, 198, 185	⊢
	: , : , :
168	assumption		⊢
169	theorem		⊢
	proveit.numbers.division.div_real_closure
170	instantiation	206, 202, 186	⊢
	: , : , :
171	instantiation	187, 188	⊢
	:
172	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
173	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
174	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
175	instantiation	189	⊢
	: , :
176	instantiation	189	⊢
	: , :
177	instantiation	190, 192	⊢
	:
178	instantiation	191, 192	⊢
	:
179	instantiation	206, 204, 193	⊢
	: , : , :
180	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
181	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
182	instantiation	194, 197	⊢
	:
183	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
184	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
185	instantiation	195, 196	⊢
	:
186	instantiation	206, 204, 197	⊢
	: , : , :
187	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
188	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
189	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
190	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
191	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
192	instantiation	206, 198, 199	⊢
	: , : , :
193	instantiation	206, 207, 200	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.negation.int_closure
195	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
196	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
197	instantiation	206, 207, 201	⊢
	: , : , :
198	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
199	instantiation	206, 202, 203	⊢
	: , : , :
200	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
201	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
202	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
203	instantiation	206, 204, 205	⊢
	: , : , :
204	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
205	instantiation	206, 207, 208	⊢
	: , : , :
206	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
207	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
208	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements