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