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	17	⊢
2	instantiation	17, 4, 5	,  ⊢
	: , : , :
3	instantiation	202, 6	⊢
	: , : , :
4	instantiation	7, 8	,  ⊢
	: , :
5	instantiation	202, 9	⊢
	: , : , :
6	instantiation	202, 10	⊢
	: , : , :
7	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
8	instantiation	11, 12, 13, 14*	,  ⊢
	:
9	instantiation	202, 21	⊢
	: , : , :
10	instantiation	134, 37, 15, 16	⊢
	: , : , : , :
11	theorem		⊢
	proveit.numbers.exponentiation.unit_complex_polar_num_neq_one
12	instantiation	131, 52, 43	⊢
	: , : , :
13	instantiation	17, 18, 19	,  ⊢
	: , : , :
14	instantiation	36, 20	⊢
	: , :
15	instantiation	36, 26	⊢
	: , :
16	instantiation	36, 21	⊢
	: , :
17	theorem		⊢
	proveit.logic.equality.sub_left_side_into
18	instantiation	22, 23, 213, 24	,  ⊢
	: , :
19	instantiation	134, 25, 26, 27	⊢
	: , : , : , :
20	instantiation	202, 28	⊢
	: , : , :
21	instantiation	202, 29	⊢
	: , : , :
22	theorem		⊢
	proveit.physics.quantum.QPE._non_int_delta_b_diff
23	instantiation	30, 149, 236, 150	⊢
	: , : , : , : , :
24	assumption		⊢
25	instantiation	66, 31, 32, 33, 34*	⊢
	: , :
26	instantiation	35, 92, 113	⊢
	: , :
27	instantiation	36, 37	⊢
	: , :
28	instantiation	191, 38, 39	⊢
	: , : , :
29	instantiation	191, 40, 41	⊢
	: , : , :
30	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
31	instantiation	131, 42, 43	⊢
	: , : , :
32	instantiation	239, 217, 59	⊢
	: , : , :
33	instantiation	44, 238, 53, 159, 45	⊢
	: , :
34	instantiation	191, 46, 47	⊢
	: , : , :
35	theorem		⊢
	proveit.numbers.addition.commutation
36	theorem		⊢
	proveit.logic.equality.equals_reversal
37	instantiation	202, 48	⊢
	: , : , :
38	instantiation	103, 149, 238, 236, 150, 53, 211, 171, 49, 107	⊢
	: , : , : , : , : , : , :
39	instantiation	104, 236, 98, 149, 85, 150, 49, 211, 171, 107	⊢
	: , : , : , : , : , :
40	instantiation	202, 50	⊢
	: , : , :
41	instantiation	51, 149, 238, 150, 151, 185, 152, 153, 127*	⊢
	: , : , : , : , :
42	instantiation	239, 217, 52	⊢
	: , : , :
43	instantiation	147, 149, 238, 236, 150, 53, 211, 171, 107	⊢
	: , : , : , : , : , :
44	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
45	instantiation	239, 176, 143	⊢
	: , : , :
46	instantiation	202, 54	⊢
	: , : , :
47	instantiation	191, 55, 56	⊢
	: , : , :
48	instantiation	202, 57	⊢
	: , : , :
49	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
50	instantiation	202, 58	⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
52	instantiation	181, 59, 121	⊢
	: , :
53	instantiation	172	⊢
	: , :
54	instantiation	60, 211, 171, 138, 130, 123, 61*	⊢
	: , : , :
55	instantiation	191, 62, 63	⊢
	: , : , :
56	instantiation	191, 64, 65	⊢
	: , : , :
57	instantiation	66, 152, 67, 68, 69*	⊢
	: , :
58	instantiation	70, 185, 114, 71*	⊢
	: , :
59	instantiation	181, 218, 187	⊢
	: , :
60	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
61	instantiation	72, 159, 209, 73*	⊢
	: , :
62	instantiation	191, 74, 75	⊢
	: , : , :
63	instantiation	191, 76, 77	⊢
	: , : , :
64	instantiation	148, 149, 98, 150, 100, 171, 107, 106	⊢
	: , : , : , :
65	instantiation	191, 78, 79	⊢
	: , : , :
66	theorem		⊢
	proveit.numbers.division.div_as_mult
67	instantiation	239, 217, 80	⊢
	: , : , :
68	instantiation	156, 95	⊢
	:
69	instantiation	81, 211, 128, 138, 130, 82*	⊢
	: , : , :
70	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
71	instantiation	201, 114	⊢
	:
72	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
73	instantiation	144, 211	⊢
	:
74	instantiation	147, 149, 98, 236, 150, 85, 211, 171, 107, 83	⊢
	: , : , : , : , : , :
75	instantiation	147, 98, 238, 149, 85, 84, 150, 211, 171, 107, 101, 106	⊢
	: , : , : , : , : , :
76	instantiation	103, 149, 98, 236, 150, 85, 211, 171, 107, 101, 106	⊢
	: , : , : , : , : , : , :
77	instantiation	191, 86, 87	⊢
	: , : , :
78	instantiation	191, 88, 89	⊢
	: , : , :
79	instantiation	90, 236, 238, 149, 91, 150, 185, 92, 113, 93*, 94*	⊢
	: , : , : , : , : , :
80	instantiation	154, 155, 95	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
82	instantiation	110, 114, 185, 96*	⊢
	: , :
83	instantiation	97, 101, 106	⊢
	: , :
84	instantiation	172	⊢
	: , :
85	instantiation	115	⊢
	: , : , :
86	instantiation	104, 149, 238, 98, 150, 99, 100, 101, 211, 171, 107, 106	⊢
	: , : , : , : , : , :
87	instantiation	202, 102	⊢
	: , : , :
88	instantiation	103, 236, 149, 150, 171, 107, 106	⊢
	: , : , : , : , : , : , :
89	instantiation	104, 149, 238, 236, 150, 105, 171, 106, 107, 108*	⊢
	: , : , : , : , : , :
90	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
91	instantiation	172	⊢
	: , :
92	instantiation	109, 111	⊢
	:
93	instantiation	110, 185, 111, 112*	⊢
	: , :
94	instantiation	201, 113	⊢
	:
95	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
96	instantiation	210, 114	⊢
	:
97	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
98	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
99	instantiation	172	⊢
	: , :
100	instantiation	115	⊢
	: , : , :
101	instantiation	239, 217, 116	⊢
	: , : , :
102	instantiation	131, 117, 118	⊢
	: , : , :
103	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
104	theorem		⊢
	proveit.numbers.multiplication.association
105	instantiation	172	⊢
	: , :
106	instantiation	119, 171, 120	⊢
	: , :
107	instantiation	239, 217, 121	⊢
	: , : , :
108	instantiation	122, 171, 196, 138, 123, 124*, 125*	⊢
	: , : , :
109	theorem		⊢
	proveit.numbers.negation.complex_closure
110	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
111	instantiation	239, 217, 165	⊢
	: , : , :
112	instantiation	191, 126, 127	⊢
	: , : , :
113	instantiation	239, 217, 141	⊢
	: , : , :
114	instantiation	239, 217, 128	⊢
	: , : , :
115	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
116	instantiation	129, 196, 218, 130	⊢
	: , :
117	instantiation	131, 132, 133	⊢
	: , : , :
118	instantiation	134, 135, 136, 137	⊢
	: , : , : , :
119	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
120	instantiation	239, 217, 138	⊢
	: , : , :
121	instantiation	139, 140, 141	⊢
	: , :
122	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
123	instantiation	142, 143	⊢
	:
124	instantiation	144, 171	⊢
	:
125	instantiation	191, 145, 146	⊢
	: , : , :
126	instantiation	147, 236, 238, 149, 151, 150, 185, 152, 153	⊢
	: , : , : , : , : , :
127	instantiation	148, 149, 238, 150, 151, 152, 153	⊢
	: , : , : , :
128	instantiation	154, 155, 231	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.division.div_real_closure
130	instantiation	156, 230	⊢
	:
131	theorem		⊢
	proveit.logic.equality.sub_right_side_into
132	instantiation	157, 185, 158, 159	⊢
	: , : , : , : , :
133	instantiation	191, 160, 161	⊢
	: , : , :
134	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
135	instantiation	202, 162	⊢
	: , : , :
136	instantiation	202, 162	⊢
	: , : , :
137	instantiation	210, 185	⊢
	:
138	instantiation	239, 224, 163	⊢
	: , : , :
139	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
140	instantiation	164, 165	⊢
	:
141	instantiation	166, 167	⊢
	:
142	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
143	instantiation	239, 168, 199	⊢
	: , : , :
144	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
145	instantiation	202, 169	⊢
	: , : , :
146	instantiation	170, 171	⊢
	:
147	theorem		⊢
	proveit.numbers.multiplication.disassociation
148	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
149	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
150	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
151	instantiation	172	⊢
	: , :
152	instantiation	239, 217, 182	⊢
	: , : , :
153	instantiation	239, 217, 183	⊢
	: , : , :
154	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
155	instantiation	173, 174	⊢
	: , :
156	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
157	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
158	instantiation	239, 176, 175	⊢
	: , : , :
159	instantiation	239, 176, 177	⊢
	: , : , :
160	instantiation	202, 178	⊢
	: , : , :
161	instantiation	202, 179	⊢
	: , : , :
162	instantiation	204, 185	⊢
	:
163	instantiation	239, 232, 180	⊢
	: , : , :
164	theorem		⊢
	proveit.numbers.negation.real_closure
165	instantiation	181, 182, 183	⊢
	: , :
166	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
167	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
168	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
169	instantiation	184, 185, 186	⊢
	: , :
170	theorem		⊢
	proveit.numbers.exponentiation.exp_zero_eq_one
171	instantiation	239, 217, 187	⊢
	: , : , :
172	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
173	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
174	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
175	instantiation	239, 189, 188	⊢
	: , : , :
176	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
177	instantiation	239, 189, 215	⊢
	: , : , :
178	instantiation	202, 190	⊢
	: , : , :
179	instantiation	191, 192, 193	⊢
	: , : , :
180	instantiation	234, 228	⊢
	:
181	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
182	instantiation	239, 224, 194	⊢
	: , : , :
183	instantiation	239, 224, 195	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
185	instantiation	239, 217, 196	⊢
	: , : , :
186	instantiation	197	⊢
	:
187	instantiation	239, 198, 199	⊢
	: , : , :
188	instantiation	239, 221, 200	⊢
	: , : , :
189	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
190	instantiation	201, 211	⊢
	:
191	axiom		⊢
	proveit.logic.equality.equals_transitivity
192	instantiation	202, 203	⊢
	: , : , :
193	instantiation	204, 211	⊢
	:
194	instantiation	239, 232, 205	⊢
	: , : , :
195	instantiation	239, 206, 207	⊢
	: , : , :
196	instantiation	239, 224, 208	⊢
	: , : , :
197	axiom		⊢
	proveit.logic.equality.equals_reflexivity
198	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
199	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
200	instantiation	239, 229, 209	⊢
	: , : , :
201	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
202	axiom		⊢
	proveit.logic.equality.substitution
203	instantiation	210, 211	⊢
	:
204	theorem		⊢
	proveit.numbers.division.frac_one_denom
205	instantiation	239, 212, 213	⊢
	: , : , :
206	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
207	instantiation	214, 215, 216	⊢
	: , :
208	instantiation	239, 232, 228	⊢
	: , : , :
209	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
210	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
211	instantiation	239, 217, 218	⊢
	: , : , :
212	instantiation	219, 220, 235	⊢
	: , :
213	assumption		⊢
214	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
215	instantiation	239, 221, 222	⊢
	: , : , :
216	instantiation	234, 223	⊢
	:
217	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
218	instantiation	239, 224, 225	⊢
	: , : , :
219	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
220	instantiation	226, 227, 228	⊢
	: , :
221	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
222	instantiation	239, 229, 230	⊢
	: , : , :
223	instantiation	239, 240, 231	⊢
	: , : , :
224	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
225	instantiation	239, 232, 233	⊢
	: , : , :
226	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
227	instantiation	234, 235	⊢
	:
228	instantiation	239, 237, 236	⊢
	: , : , :
229	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
230	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
231	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
232	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
233	instantiation	239, 237, 238	⊢
	: , : , :
234	theorem		⊢
	proveit.numbers.negation.int_closure
235	instantiation	239, 240, 241	⊢
	: , : , :
236	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
237	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
238	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
239	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
240	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
241	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
*equality replacement requirements