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