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