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	283	⊢
2	instantiation	301, 335, 4, 5, 6, 7	⊢
	: , : , : , :
3	instantiation	73, 74, 8, 9	⊢
	: , : , :
4	instantiation	316	⊢
	: , :
5	instantiation	316	⊢
	: , :
6	instantiation	13, 153, 10, 15*, 11*, 12*	⊢
	: , :
7	instantiation	13, 153, 14, 15*, 16*, 17*	⊢
	: , :
8	instantiation	293, 18, 19	⊢
	:
9	instantiation	333, 325, 20	⊢
	: , : , :
10	instantiation	182, 131, 113	⊢
	: , : , :
11	instantiation	157, 21	⊢
	: , :
12	instantiation	283, 22, 23	⊢
	: , : , :
13	theorem		⊢
	proveit.trigonometry.complex_unit_circle_chord_length
14	instantiation	182, 136, 123	⊢
	: , : , :
15	instantiation	283, 24, 25	⊢
	: , : , :
16	instantiation	157, 26	⊢
	: , :
17	instantiation	283, 27, 28	⊢
	: , : , :
18	instantiation	333, 325, 45	⊢
	: , : , :
19	instantiation	29, 30	⊢
	: , :
20	instantiation	31, 32	⊢
	:
21	instantiation	224, 33	⊢
	: , : , :
22	instantiation	224, 34	⊢
	: , : , :
23	instantiation	283, 35, 36	⊢
	: , : , :
24	instantiation	224, 37	⊢
	: , : , :
25	instantiation	38, 39	⊢
	:
26	instantiation	224, 40	⊢
	: , : , :
27	instantiation	224, 41	⊢
	: , : , :
28	instantiation	283, 42, 43	⊢
	: , : , :
29	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
30	instantiation	44, 153, 45, 46	⊢
	: , :
31	theorem		⊢
	proveit.trigonometry.real_closure
32	instantiation	182, 102, 85	⊢
	: , : , :
33	instantiation	283, 47, 48	⊢
	: , : , :
34	instantiation	283, 49, 50	⊢
	: , : , :
35	instantiation	283, 51, 52	⊢
	: , : , :
36	instantiation	60, 67	⊢
	:
37	instantiation	189, 69	⊢
	:
38	theorem		⊢
	proveit.numbers.exponentiation.exp_zero_eq_one
39	instantiation	333, 325, 53	⊢
	: , : , :
40	instantiation	283, 54, 55	⊢
	: , : , :
41	instantiation	283, 56, 57	⊢
	: , : , :
42	instantiation	283, 58, 59	⊢
	: , : , :
43	instantiation	60, 76	⊢
	:
44	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq
45	instantiation	61, 153, 297, 63	⊢
	: , : , :
46	instantiation	62, 153, 297, 63	⊢
	: , : , :
47	instantiation	118, 241, 335, 242, 146, 147, 319, 199, 69, 294, 246	⊢
	: , : , : , : , : , : , :
48	instantiation	100, 328, 327, 241, 80, 242, 69, 319, 199, 294, 246	⊢
	: , : , : , : , : , :
49	instantiation	224, 64	⊢
	: , : , :
50	instantiation	226, 95, 65*	⊢
	:
51	instantiation	224, 66	⊢
	: , : , :
52	instantiation	73, 74, 75, 67, 305*	⊢
	: , : , :
53	instantiation	333, 249, 68	⊢
	: , : , :
54	instantiation	118, 241, 335, 328, 242, 146, 319, 199, 69, 294	⊢
	: , : , : , : , : , : , :
55	instantiation	100, 328, 119, 241, 88, 242, 69, 319, 199, 294	⊢
	: , : , : , : , : , :
56	instantiation	224, 70	⊢
	: , : , :
57	instantiation	226, 105, 71*	⊢
	:
58	instantiation	224, 72	⊢
	: , : , :
59	instantiation	73, 74, 75, 76, 305*	⊢
	: , : , :
60	theorem		⊢
	proveit.numbers.division.frac_one_denom
61	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
62	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
63	instantiation	77, 78	⊢
	:
64	instantiation	172, 79	⊢
	:
65	instantiation	206, 287, 80, 319, 199, 294, 246, 81*	⊢
	: , :
66	instantiation	283, 82, 83	⊢
	: , : , :
67	instantiation	182, 84, 85	⊢
	: , : , :
68	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
69	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
70	instantiation	172, 86	⊢
	:
71	instantiation	206, 87, 88, 319, 199, 294, 116*, 117*	⊢
	: , :
72	instantiation	100, 328, 335, 241, 99, 242, 319, 199, 200	⊢
	: , : , : , : , : , :
73	theorem		⊢
	proveit.numbers.division.frac_cancel_left
74	instantiation	333, 90, 89	⊢
	: , : , :
75	instantiation	333, 90, 91	⊢
	: , : , :
76	instantiation	333, 325, 93	⊢
	: , : , :
77	theorem		⊢
	proveit.trigonometry.sine_pos_interval
78	instantiation	92, 153, 222, 93, 94	⊢
	: , : , :
79	instantiation	104, 95	⊢
	:
80	instantiation	96	⊢
	: , : , : , :
81	instantiation	283, 97, 98	⊢
	: , : , :
82	instantiation	118, 241, 328, 335, 242, 99, 246, 319, 199, 200	⊢
	: , : , : , : , : , : , :
83	instantiation	100, 328, 119, 241, 101, 242, 319, 246, 199, 200	⊢
	: , : , : , : , : , :
84	instantiation	333, 325, 102	⊢
	: , : , :
85	instantiation	186, 241, 335, 328, 242, 103, 246, 199, 200	⊢
	: , : , : , : , : , :
86	instantiation	104, 105	⊢
	:
87	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
88	instantiation	135	⊢
	: , : , :
89	instantiation	333, 107, 106	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
91	instantiation	333, 107, 108	⊢
	: , : , :
92	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
93	instantiation	333, 249, 127	⊢
	: , : , :
94	instantiation	109, 110, 111	⊢
	: , :
95	instantiation	182, 112, 113	⊢
	: , : , :
96	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
97	instantiation	301, 119, 114, 115, 116, 117, 208	⊢
	: , : , : , :
98	instantiation	118, 241, 119, 242, 120, 319, 199, 200, 246	⊢
	: , : , : , : , : , : , :
99	instantiation	316	⊢
	: , :
100	theorem		⊢
	proveit.numbers.multiplication.association
101	instantiation	135	⊢
	: , : , :
102	instantiation	210, 121, 223	⊢
	: , :
103	instantiation	316	⊢
	: , :
104	theorem		⊢
	proveit.numbers.negation.complex_closure
105	instantiation	182, 122, 123	⊢
	: , : , :
106	instantiation	333, 125, 124	⊢
	: , : , :
107	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
108	instantiation	333, 125, 126	⊢
	: , : , :
109	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
110	instantiation	209, 127	⊢
	:
111	instantiation	128, 129, 130	⊢
	: , : , :
112	instantiation	333, 325, 131	⊢
	: , : , :
113	instantiation	283, 132, 133	⊢
	: , : , :
114	instantiation	135	⊢
	: , : , :
115	instantiation	135	⊢
	: , : , :
116	instantiation	229, 134	⊢
	:
117	instantiation	229, 167	⊢
	:
118	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
119	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
120	instantiation	135	⊢
	: , : , :
121	instantiation	210, 273, 222	⊢
	: , :
122	instantiation	333, 325, 136	⊢
	: , : , :
123	instantiation	186, 241, 335, 328, 242, 146, 319, 199, 294	⊢
	: , : , : , : , : , :
124	instantiation	333, 137, 315	⊢
	: , : , :
125	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
126	instantiation	333, 137, 299	⊢
	: , : , :
127	instantiation	138, 248, 250	⊢
	: , :
128	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
129	instantiation	182, 139, 163	⊢
	: , : , :
130	instantiation	193, 191, 140, 141, 142*, 143*	⊢
	: , : , :
131	instantiation	210, 160, 144	⊢
	: , :
132	instantiation	186, 328, 335, 241, 147, 242, 145, 294, 246	⊢
	: , : , : , : , : , :
133	instantiation	186, 241, 335, 242, 146, 147, 319, 199, 294, 246	⊢
	: , : , : , : , : , :
134	instantiation	148, 335	⊢
	:
135	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
136	instantiation	210, 160, 312	⊢
	: , :
137	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
138	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
139	instantiation	149, 150, 151	⊢
	: , : , :
140	instantiation	210, 211, 153	⊢
	: , :
141	instantiation	152, 211, 153, 222, 185, 154	⊢
	: , : , :
142	instantiation	283, 155, 156	⊢
	: , : , :
143	instantiation	157, 158, 159*	⊢
	: , :
144	instantiation	210, 312, 273	⊢
	: , :
145	instantiation	333, 325, 160	⊢
	: , : , :
146	instantiation	316	⊢
	: , :
147	instantiation	316	⊢
	: , :
148	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
149	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
150	instantiation	161, 162, 163	⊢
	: , : , :
151	instantiation	164, 222, 165, 278, 166, 167, 168*, 169*	⊢
	: , : , :
152	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
153	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
154	instantiation	170, 260	⊢
	:
155	instantiation	224, 171	⊢
	: , : , :
156	instantiation	172, 173	⊢
	:
157	theorem		⊢
	proveit.logic.equality.equals_reversal
158	instantiation	174, 241, 335, 328, 242, 175, 190, 199	⊢
	: , : , : , : , : , :
159	instantiation	283, 176, 177	⊢
	: , : , :
160	instantiation	210, 326, 222	⊢
	: , :
161	theorem		⊢
	proveit.logic.equality.sub_left_side_into
162	instantiation	178, 328, 248, 250, 179, 180*	⊢
	: , : , : , : , : , :
163	instantiation	224, 181	⊢
	: , : , :
164	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
165	instantiation	210, 273, 223	⊢
	: , :
166	instantiation	182, 183, 184	⊢
	: , : , :
167	instantiation	257, 185	⊢
	: , :
168	instantiation	186, 328, 335, 241, 187, 242, 199, 246, 200	⊢
	: , : , : , : , : , :
169	instantiation	188, 199, 190	⊢
	: , :
170	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
171	instantiation	189, 190	⊢
	:
172	theorem		⊢
	proveit.numbers.addition.elim_zero_left
173	instantiation	333, 325, 191	⊢
	: , : , :
174	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
175	instantiation	316	⊢
	: , :
176	instantiation	224, 192	⊢
	: , : , :
177	instantiation	317, 199	⊢
	:
178	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
179	instantiation	193, 272, 326, 194, 195, 196*, 197*	⊢
	: , : , :
180	instantiation	198, 328, 199, 200	⊢
	: , : , : , :
181	instantiation	283, 201, 202	⊢
	: , : , :
182	theorem		⊢
	proveit.logic.equality.sub_right_side_into
183	instantiation	203, 204, 205	⊢
	: , :
184	instantiation	206, 315, 207, 246, 294, 208*	⊢
	: , :
185	instantiation	209, 248	⊢
	:
186	theorem		⊢
	proveit.numbers.multiplication.disassociation
187	instantiation	316	⊢
	: , :
188	theorem		⊢
	proveit.numbers.multiplication.commutation
189	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
190	instantiation	333, 325, 278	⊢
	: , : , :
191	instantiation	210, 211, 222	⊢
	: , :
192	instantiation	212, 324, 332, 213*	⊢
	: , : , : , :
193	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
194	instantiation	333, 329, 214	⊢
	: , : , :
195	instantiation	215, 326, 273, 297, 216, 217	⊢
	: , : , :
196	instantiation	218, 252, 319, 219	⊢
	: , : , :
197	instantiation	283, 220, 221	⊢
	: , : , :
198	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
199	instantiation	333, 325, 222	⊢
	: , : , :
200	instantiation	333, 325, 223	⊢
	: , : , :
201	instantiation	224, 225	⊢
	: , : , :
202	instantiation	226, 294	⊢
	:
203	theorem		⊢
	proveit.numbers.absolute_value.weak_upper_bound
204	instantiation	227, 255, 278, 256	⊢
	: , : , :
205	instantiation	257, 228	⊢
	: , :
206	theorem		⊢
	proveit.numbers.absolute_value.abs_prod
207	instantiation	316	⊢
	: , :
208	instantiation	229, 230	⊢
	:
209	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
210	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
211	instantiation	333, 329, 231	⊢
	: , : , :
212	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
213	instantiation	283, 232, 233	⊢
	: , : , :
214	instantiation	333, 331, 234	⊢
	: , : , :
215	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
216	instantiation	235, 326, 297, 236, 237, 238, 239*	⊢
	: , : , :
217	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
218	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
219	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
220	instantiation	240, 241, 335, 328, 242, 243, 246, 252, 244	⊢
	: , : , : , : , : , :
221	instantiation	245, 252, 246, 247	⊢
	: , : , :
222	instantiation	333, 249, 248	⊢
	: , : , :
223	instantiation	333, 249, 250	⊢
	: , : , :
224	axiom		⊢
	proveit.logic.equality.substitution
225	instantiation	251, 252, 294, 253*	⊢
	: , :
226	theorem		⊢
	proveit.numbers.absolute_value.abs_even
227	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
228	instantiation	254, 255, 278, 256	⊢
	: , : , :
229	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
230	instantiation	257, 258	⊢
	: , :
231	instantiation	333, 259, 260	⊢
	: , : , :
232	instantiation	301, 335, 261, 262, 263, 264	⊢
	: , : , : , :
233	instantiation	265, 266, 267	⊢
	:
234	instantiation	333, 334, 268	⊢
	: , : , :
235	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
236	instantiation	291, 292, 270	⊢
	: , : , :
237	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
238	instantiation	269, 270	⊢
	:
239	instantiation	271, 319	⊢
	:
240	theorem		⊢
	proveit.numbers.addition.disassociation
241	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
242	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
243	instantiation	316	⊢
	: , :
244	instantiation	333, 325, 272	⊢
	: , : , :
245	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
246	instantiation	333, 325, 273	⊢
	: , : , :
247	instantiation	274	⊢
	:
248	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
249	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
250	instantiation	275, 276	⊢
	:
251	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
252	instantiation	333, 325, 297	⊢
	: , : , :
253	instantiation	317, 294	⊢
	:
254	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
255	instantiation	277, 278	⊢
	:
256	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
257	theorem		⊢
	proveit.numbers.ordering.relax_less
258	instantiation	279, 308	⊢
	:
259	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
260	instantiation	280, 281, 282	⊢
	: , :
261	instantiation	316	⊢
	: , :
262	instantiation	316	⊢
	: , :
263	instantiation	283, 284, 285	⊢
	: , : , :
264	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
265	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
266	instantiation	333, 325, 286	⊢
	: , : , :
267	instantiation	314, 287	⊢
	:
268	instantiation	288, 289, 328	⊢
	: , :
269	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
270	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
271	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
272	instantiation	333, 329, 290	⊢
	: , : , :
273	instantiation	291, 292, 308	⊢
	: , : , :
274	axiom		⊢
	proveit.logic.equality.equals_reflexivity
275	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
276	instantiation	293, 294, 295	⊢
	:
277	theorem		⊢
	proveit.numbers.negation.real_closure
278	instantiation	296, 297, 326, 298	⊢
	: , :
279	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
280	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
281	instantiation	333, 300, 299	⊢
	: , : , :
282	instantiation	333, 300, 315	⊢
	: , : , :
283	axiom		⊢
	proveit.logic.equality.equals_transitivity
284	instantiation	301, 335, 302, 303, 304, 305	⊢
	: , : , : , :
285	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
286	instantiation	333, 329, 306	⊢
	: , : , :
287	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
288	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
289	instantiation	333, 307, 308	⊢
	: , : , :
290	instantiation	333, 331, 309	⊢
	: , : , :
291	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
292	instantiation	310, 311	⊢
	: , :
293	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
294	instantiation	333, 325, 312	⊢
	: , : , :
295	assumption		⊢
296	theorem		⊢
	proveit.numbers.division.div_real_closure
297	instantiation	333, 329, 313	⊢
	: , : , :
298	instantiation	314, 315	⊢
	:
299	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
300	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
301	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
302	instantiation	316	⊢
	: , :
303	instantiation	316	⊢
	: , :
304	instantiation	317, 319	⊢
	:
305	instantiation	318, 319	⊢
	:
306	instantiation	333, 331, 320	⊢
	: , : , :
307	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
308	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
309	instantiation	321, 324	⊢
	:
310	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
311	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
312	instantiation	322, 323	⊢
	:
313	instantiation	333, 331, 324	⊢
	: , : , :
314	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
315	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
316	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
317	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
318	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
319	instantiation	333, 325, 326	⊢
	: , : , :
320	instantiation	333, 334, 327	⊢
	: , : , :
321	theorem		⊢
	proveit.numbers.negation.int_closure
322	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
323	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
324	instantiation	333, 334, 328	⊢
	: , : , :
325	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
326	instantiation	333, 329, 330	⊢
	: , : , :
327	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
328	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
329	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
330	instantiation	333, 331, 332	⊢
	: , : , :
331	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
332	instantiation	333, 334, 335	⊢
	: , : , :
333	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
334	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
335	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements