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