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	theorem		⊢
	proveit.logic.equality.sub_right_side_into
2	instantiation	196, 4, 5	⊢
	: , : , :
3	instantiation	191, 6, 7, 8	⊢
	: , : , : , :
4	instantiation	9, 10, 11	⊢
	: , : , :
5	instantiation	12, 287	⊢
	:
6	instantiation	212, 13	⊢
	: , : , :
7	instantiation	212, 14	⊢
	: , : , :
8	instantiation	210, 15	⊢
	: , :
9	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
10	instantiation	136, 20, 16, 19, 17	⊢
	: , : , :
11	instantiation	18, 19, 20, 21, 22	⊢
	: , : , :
12	theorem		⊢
	proveit.physics.quantum.QPE._fail_sum
13	instantiation	156, 23, 24	⊢
	: , : , :
14	instantiation	156, 25, 26	⊢
	: , : , :
15	instantiation	27, 288, 298, 206, 28, 207, 63, 29, 30	⊢
	: , : , : , : , : , :
16	modus ponens	31, 32	⊢
17	modus ponens	33, 34	⊢
18	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
19	modus ponens	35, 36	⊢
20	modus ponens	37, 38	⊢
21	modus ponens	39, 40	⊢
22	modus ponens	41, 42	⊢
23	instantiation	212, 43	⊢
	: , : , :
24	instantiation	210, 44	⊢
	: , :
25	instantiation	212, 45	⊢
	: , : , :
26	instantiation	210, 46	⊢
	: , :
27	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
28	instantiation	102	⊢
	: , :
29	modus ponens	47, 76	⊢
30	modus ponens	48, 80	⊢
31	instantiation	53	⊢
	: , : , :
32	generalization	49	⊢
33	instantiation	55	⊢
	: , : , :
34	generalization	50	⊢
35	instantiation	53	⊢
	: , : , :
36	generalization	51	⊢
37	instantiation	53	⊢
	: , : , :
38	generalization	52	⊢
39	instantiation	53	⊢
	: , : , :
40	generalization	54	⊢
41	instantiation	55	⊢
	: , : , :
42	generalization	56	⊢
43	modus ponens	57, 58	⊢
44	instantiation	59, 207, 63	⊢
	: , :
45	modus ponens	60, 61	⊢
46	instantiation	62, 207, 63	⊢
	: , :
47	instantiation	64	⊢
	: , : , :
48	instantiation	64	⊢
	: , : , :
49	instantiation	132, 65, 298	,  ⊢
	: , :
50	instantiation	72, 66, 185	,  ⊢
	:
51	instantiation	122, 260, 67, 68	,  ⊢
	: , :
52	instantiation	132, 69, 298	,  ⊢
	: , :
53	theorem		⊢
	proveit.numbers.summation.summation_real_closure
54	instantiation	122, 260, 70, 71	,  ⊢
	: , :
55	theorem		⊢
	proveit.numbers.summation.weak_summation_from_summands_bound
56	instantiation	72, 73, 190	,  ⊢
	:
57	instantiation	77, 266	⊢
	: , : , : , : , : , : , :
58	generalization	74	⊢
59	modus ponens	75, 76	⊢
60	instantiation	77, 266	⊢
	: , : , : , : , : , : , :
61	generalization	78	⊢
62	modus ponens	79, 80	⊢
63	instantiation	296, 259, 81	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.summation.summation_complex_closure
65	instantiation	296, 84, 82	,  ⊢
	: , : , :
66	instantiation	88, 234, 290, 199, 83	,  ⊢
	: , : , :
67	instantiation	202, 95, 118	,  ⊢
	: , :
68	instantiation	86, 298, 87, 108, 130	,  ⊢
	: , :
69	instantiation	296, 84, 85	,  ⊢
	: , : , :
70	instantiation	202, 95, 123	,  ⊢
	: , :
71	instantiation	86, 298, 87, 108, 134	,  ⊢
	: , :
72	theorem		⊢
	proveit.physics.quantum.QPE._alpha_sqrd_upper_bound
73	instantiation	88, 234, 290, 222, 89	,  ⊢
	: , : , :
74	instantiation	210, 90	,  ⊢
	: , :
75	instantiation	93, 288, 266, 206	⊢
	: , : , : , : , : , :
76	generalization	91	⊢
77	theorem		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
78	instantiation	210, 92	,  ⊢
	: , :
79	instantiation	93, 288, 266, 206	⊢
	: , : , : , : , : , :
80	generalization	94	⊢
81	instantiation	122, 260, 95, 96	⊢
	: , :
82	instantiation	100, 97	,  ⊢
	:
83	instantiation	103, 98, 99	,  ⊢
	: , :
84	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
85	instantiation	100, 101	,  ⊢
	:
86	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
87	instantiation	102	⊢
	: , :
88	theorem		⊢
	proveit.numbers.number_sets.integers.in_interval
89	instantiation	103, 104, 105	,  ⊢
	: , :
90	instantiation	107, 244, 108, 130, 109*	,  ⊢
	: , : , : , :
91	instantiation	296, 259, 106	,  ⊢
	: , : , :
92	instantiation	107, 244, 108, 134, 109*	,  ⊢
	: , : , : , :
93	theorem		⊢
	proveit.numbers.multiplication.distribute_through_summation
94	instantiation	296, 259, 110	,  ⊢
	: , : , :
95	instantiation	296, 269, 111	⊢
	: , : , :
96	instantiation	247, 151	⊢
	:
97	instantiation	114, 112	,  ⊢
	:
98	instantiation	284, 234, 235, 236	,  ⊢
	: , : , :
99	instantiation	116, 113	,  ⊢
	: , :
100	theorem		⊢
	proveit.numbers.absolute_value.abs_complex_closure
101	instantiation	114, 115	,  ⊢
	:
102	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
103	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
104	instantiation	116, 117	,  ⊢
	: , :
105	instantiation	233, 254, 290, 255	,  ⊢
	: , : , :
106	instantiation	122, 260, 118, 119	,  ⊢
	: , :
107	theorem		⊢
	proveit.numbers.division.prod_of_fracs
108	instantiation	296, 248, 120	⊢
	: , : , :
109	instantiation	121, 244	⊢
	:
110	instantiation	122, 260, 123, 124	,  ⊢
	: , :
111	instantiation	296, 276, 125	⊢
	: , : , :
112	instantiation	128, 221, 199	,  ⊢
	: , :
113	instantiation	126, 201, 127	,  ⊢
	: , : , :
114	theorem		⊢
	proveit.physics.quantum.QPE._alpha_are_complex
115	instantiation	128, 221, 222	,  ⊢
	: , :
116	theorem		⊢
	proveit.numbers.ordering.relax_less
117	instantiation	216, 129, 223	,  ⊢
	: , : , :
118	instantiation	132, 162, 298	,  ⊢
	: , :
119	instantiation	133, 130	,  ⊢
	:
120	instantiation	296, 262, 131	⊢
	: , : , :
121	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
122	theorem		⊢
	proveit.numbers.division.div_real_closure
123	instantiation	132, 164, 298	,  ⊢
	: , :
124	instantiation	133, 134	,  ⊢
	:
125	instantiation	296, 297, 135	⊢
	: , : , :
126	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
127	instantiation	252, 293	⊢
	:
128	theorem		⊢
	proveit.physics.quantum.QPE._mod_add_closure
129	instantiation	136, 155, 260, 137, 138, 139*, 140*	⊢
	: , : , :
130	instantiation	143, 141, 228	,  ⊢
	: , :
131	instantiation	296, 271, 142	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
133	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_if_in_complex_nonzero
134	instantiation	143, 144, 228	,  ⊢
	: , :
135	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
136	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
137	instantiation	256, 257, 293	⊢
	: , : , :
138	instantiation	145, 293	⊢
	:
139	instantiation	224, 244, 146	⊢
	: , :
140	instantiation	156, 147, 148	⊢
	: , : , :
141	instantiation	152, 149, 150	,  ⊢
	:
142	instantiation	296, 277, 151	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_nonzero_closure
144	instantiation	152, 153, 154	,  ⊢
	:
145	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
146	instantiation	296, 259, 155	⊢
	: , : , :
147	instantiation	156, 157, 158	⊢
	: , : , :
148	instantiation	159, 160, 161	⊢
	: , :
149	instantiation	296, 259, 162	,  ⊢
	: , : , :
150	instantiation	165, 163	,  ⊢
	: , :
151	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
152	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
153	instantiation	296, 259, 164	,  ⊢
	: , : , :
154	instantiation	165, 166	,  ⊢
	: , :
155	instantiation	296, 269, 167	⊢
	: , : , :
156	axiom		⊢
	proveit.logic.equality.equals_transitivity
157	instantiation	212, 180	⊢
	: , : , :
158	instantiation	212, 168	⊢
	: , : , :
159	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
160	instantiation	169, 170, 171	⊢
	: , :
161	instantiation	172	⊢
	:
162	instantiation	175, 173, 177	,  ⊢
	: , :
163	instantiation	178, 174	,  ⊢
	: , :
164	instantiation	175, 176, 177	,  ⊢
	: , :
165	theorem		⊢
	proveit.numbers.addition.subtraction.nonzero_difference_if_different
166	instantiation	178, 179	,  ⊢
	: , :
167	instantiation	296, 276, 250	⊢
	: , : , :
168	instantiation	212, 180	⊢
	: , : , :
169	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
170	instantiation	181, 244, 182, 183	⊢
	: , :
171	instantiation	296, 259, 203	⊢
	: , : , :
172	axiom		⊢
	proveit.logic.equality.equals_reflexivity
173	instantiation	296, 269, 184	,  ⊢
	: , : , :
174	instantiation	188, 189, 199, 185	,  ⊢
	: , :
175	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
176	instantiation	296, 269, 186	,  ⊢
	: , : , :
177	instantiation	246, 187	⊢
	:
178	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
179	instantiation	188, 189, 222, 190	,  ⊢
	: , :
180	instantiation	191, 192, 193, 194	⊢
	: , : , : , :
181	theorem		⊢
	proveit.numbers.division.div_complex_closure
182	instantiation	195, 228, 244	⊢
	: , :
183	instantiation	196, 230, 197	⊢
	: , : , :
184	instantiation	296, 276, 199	,  ⊢
	: , : , :
185	instantiation	198, 199, 200, 201	,  ⊢
	: , :
186	instantiation	296, 276, 222	,  ⊢
	: , : , :
187	instantiation	202, 203, 204	⊢
	: , :
188	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_not_eq_nonzeroInt
189	instantiation	205, 206, 288, 207	⊢
	: , : , : , : , :
190	instantiation	247, 208	,  ⊢
	:
191	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
192	instantiation	212, 209	⊢
	: , : , :
193	instantiation	210, 211	⊢
	: , :
194	instantiation	212, 213	⊢
	: , : , :
195	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
196	theorem		⊢
	proveit.logic.equality.sub_left_side_into
197	instantiation	214, 228	⊢
	:
198	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_int
199	instantiation	296, 215, 236	,  ⊢
	: , : , :
200	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
201	instantiation	216, 217, 218	,  ⊢
	: , : , :
202	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
203	instantiation	256, 257, 219	⊢
	: , : , :
204	instantiation	220, 221	⊢
	:
205	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
206	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
207	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
208	instantiation	273, 222, 223	,  ⊢
	:
209	instantiation	224, 225, 226	⊢
	: , :
210	theorem		⊢
	proveit.logic.equality.equals_reversal
211	instantiation	227, 228, 229, 242, 230	⊢
	: , : , :
212	axiom		⊢
	proveit.logic.equality.substitution
213	instantiation	231, 232, 266	⊢
	: , :
214	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
215	instantiation	283, 234, 235	⊢
	: , :
216	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
217	instantiation	233, 234, 235, 236	,  ⊢
	: , : , :
218	instantiation	237, 238	⊢
	:
219	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
220	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
221	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
222	instantiation	296, 239, 255	,  ⊢
	: , : , :
223	instantiation	280, 240, 241	,  ⊢
	: , : , :
224	theorem		⊢
	proveit.numbers.addition.commutation
225	instantiation	296, 259, 242	⊢
	: , : , :
226	instantiation	243, 244	⊢
	:
227	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
228	instantiation	296, 259, 245	⊢
	: , : , :
229	instantiation	246, 260	⊢
	:
230	instantiation	247, 278	⊢
	:
231	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
232	instantiation	296, 248, 249	⊢
	: , : , :
233	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
234	instantiation	289, 250, 285	⊢
	: , :
235	instantiation	294, 254	⊢
	:
236	assumption		⊢
237	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
238	instantiation	251, 253	⊢
	:
239	instantiation	283, 254, 290	⊢
	: , :
240	instantiation	252, 253	⊢
	:
241	instantiation	284, 254, 290, 255	,  ⊢
	: , : , :
242	instantiation	256, 257, 258	⊢
	: , : , :
243	theorem		⊢
	proveit.numbers.negation.complex_closure
244	instantiation	296, 259, 260	⊢
	: , : , :
245	instantiation	296, 269, 261	⊢
	: , : , :
246	theorem		⊢
	proveit.numbers.negation.real_closure
247	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
248	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
249	instantiation	296, 262, 263	⊢
	: , : , :
250	instantiation	294, 290	⊢
	:
251	theorem		⊢
	proveit.numbers.negation.int_neg_closure
252	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
253	instantiation	264, 265, 266	⊢
	: , :
254	instantiation	289, 274, 285	⊢
	: , :
255	assumption		⊢
256	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
257	instantiation	267, 268	⊢
	: , :
258	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
259	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
260	instantiation	296, 269, 270	⊢
	: , : , :
261	instantiation	296, 276, 295	⊢
	: , : , :
262	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
263	instantiation	296, 271, 272	⊢
	: , : , :
264	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
265	instantiation	273, 274, 275	⊢
	:
266	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
267	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
268	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
269	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
270	instantiation	296, 276, 285	⊢
	: , : , :
271	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
272	instantiation	296, 277, 278	⊢
	: , : , :
273	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
274	instantiation	296, 279, 287	⊢
	: , : , :
275	instantiation	280, 281, 282	⊢
	: , : , :
276	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
277	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
278	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
279	instantiation	283, 285, 286	⊢
	: , :
280	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
281	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
282	instantiation	284, 285, 286, 287	⊢
	: , : , :
283	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
284	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
285	instantiation	296, 297, 288	⊢
	: , : , :
286	instantiation	289, 290, 291	⊢
	: , :
287	assumption		⊢
288	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
289	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
290	instantiation	296, 292, 293	⊢
	: , : , :
291	instantiation	294, 295	⊢
	:
292	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
293	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
294	theorem		⊢
	proveit.numbers.negation.int_closure
295	instantiation	296, 297, 298	⊢
	: , : , :
296	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
297	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
298	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements