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