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