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.numbers.ordering.transitivity_less_eq_less_eq
2	instantiation	4, 19, 5, 411, 6, 20	,  ⊢
	: , : , :
3	instantiation	7, 22, 8, 9, 10, 11*	,  ⊢
	: , : , :
4	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
5	instantiation	424, 262, 12	⊢
	: , : , :
6	instantiation	13, 318, 46, 14*	⊢
	: , :
7	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
8	instantiation	15, 192, 16, 17, 35, 249	,  ⊢
	: , :
9	instantiation	18, 19, 20	,  ⊢
	:
10	instantiation	21, 426, 331, 133, 332, 22, 23, 55, 24*	,  ⊢
	: , : , : , : , : , :
11	instantiation	240, 25, 26, 27	,  ⊢
	: , : , : , :
12	instantiation	278, 28	⊢
	:
13	theorem		⊢
	proveit.numbers.absolute_value.triangle_inequality
14	instantiation	363, 29, 30	⊢
	: , : , :
15	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure
16	instantiation	214	⊢
	: , : , :
17	instantiation	424, 119, 31	⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
19	instantiation	210, 32, 33	,  ⊢
	: , : , :
20	instantiation	34, 426, 331, 133, 332, 95, 35, 36, 37*	,  ⊢
	: , : , : , : , : , :
21	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_factor_bound
22	instantiation	424, 39, 38	⊢
	: , : , :
23	instantiation	424, 39, 40	⊢
	: , : , :
24	instantiation	363, 41, 42	⊢
	: , : , :
25	instantiation	363, 43, 44	,  ⊢
	: , : , :
26	instantiation	258	⊢
	:
27	instantiation	259, 45	,  ⊢
	: , :
28	instantiation	267, 318, 46	⊢
	: , :
29	instantiation	384, 426, 47, 48, 49, 50	⊢
	: , : , : , :
30	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
31	instantiation	424, 383, 367	⊢
	: , : , :
32	instantiation	320, 155, 72	,  ⊢
	: , :
33	instantiation	167, 331, 426, 417, 332, 133, 402, 283, 51	,  ⊢
	: , : , : , : , : , :
34	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
35	instantiation	424, 119, 52	⊢
	: , : , :
36	instantiation	53, 54, 55	,  ⊢
	: , : , :
37	instantiation	56, 426, 331, 133, 332, 402, 283	⊢
	: , : , : , :
38	instantiation	424, 57, 426	⊢
	: , : , :
39	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
40	instantiation	424, 57, 58	⊢
	: , : , :
41	instantiation	167, 426, 331, 133, 226, 332, 402, 283, 227	⊢
	: , : , : , : , : , :
42	instantiation	363, 59, 60	⊢
	: , : , :
43	instantiation	337, 61	⊢
	: , : , :
44	instantiation	304, 402, 62, 63, 64*	,  ⊢
	: , :
45	instantiation	363, 65, 66	,  ⊢
	: , : , :
46	instantiation	287, 70	⊢
	:
47	instantiation	399	⊢
	: , :
48	instantiation	399	⊢
	: , :
49	instantiation	67, 68	⊢
	:
50	instantiation	69, 70, 71*	⊢
	:
51	instantiation	424, 410, 72	,  ⊢
	: , : , :
52	instantiation	424, 383, 315	⊢
	: , : , :
53	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
54	instantiation	254, 73	,  ⊢
	:
55	instantiation	74, 75, 198, 76*	,  ⊢
	:
56	theorem		⊢
	proveit.numbers.multiplication.mult_zero_any
57	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
58	instantiation	424, 77, 315	⊢
	: , : , :
59	instantiation	224, 417, 402, 283, 227	⊢
	: , : , : , : , : , : , :
60	instantiation	225, 331, 426, 332, 386, 78, 402, 283, 227, 347*	⊢
	: , : , : , : , : , :
61	instantiation	337, 212	⊢
	: , : , :
62	instantiation	210, 79, 80	⊢
	: , : , :
63	instantiation	107, 192, 125, 152, 108, 186	,  ⊢
	: , :
64	instantiation	363, 81, 82	,  ⊢
	: , : , :
65	instantiation	337, 83	⊢
	: , : , :
66	instantiation	304, 318, 84, 85, 86*	,  ⊢
	: , :
67	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
68	instantiation	87, 417	⊢
	:
69	theorem		⊢
	proveit.numbers.absolute_value.abs_even
70	instantiation	187, 88, 89	⊢
	: , :
71	instantiation	90, 91, 92*	⊢
	:
72	instantiation	171, 252, 380, 93	,  ⊢
	: , : , :
73	instantiation	94, 95, 249	,  ⊢
	: , :
74	theorem		⊢
	proveit.trigonometry.sine_linear_bound_nonneg
75	instantiation	96, 144, 97	,  ⊢
	:
76	instantiation	363, 98, 99	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
78	instantiation	399	⊢
	: , :
79	instantiation	165, 100, 188	⊢
	: , :
80	instantiation	167, 331, 426, 417, 332, 101, 349, 283, 188	⊢
	: , : , : , : , : , :
81	instantiation	337, 102	,  ⊢
	: , : , :
82	instantiation	363, 103, 104	⊢
	: , : , :
83	instantiation	337, 212	⊢
	: , : , :
84	instantiation	210, 105, 106	⊢
	: , : , :
85	instantiation	107, 192, 159, 356, 108, 186	,  ⊢
	: , :
86	instantiation	363, 109, 110	,  ⊢
	: , : , :
87	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
88	instantiation	424, 410, 111	⊢
	: , : , :
89	instantiation	210, 112, 113	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.absolute_value.complex_unit_length
91	instantiation	210, 114, 115	⊢
	: , : , :
92	instantiation	259, 116	⊢
	: , :
93	instantiation	117, 118	,  ⊢
	:
94	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
95	instantiation	424, 119, 362	⊢
	: , : , :
96	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_real_is_real_nonneg
97	instantiation	120, 173	,  ⊢
	: , :
98	instantiation	337, 121	⊢
	: , : , :
99	instantiation	363, 122, 123	⊢
	: , : , :
100	instantiation	424, 410, 124	⊢
	: , : , :
101	instantiation	399	⊢
	: , :
102	instantiation	157, 158, 125, 349, 283, 188, 298, 350, 284, 160, 126*, 285*	,  ⊢
	: , : , :
103	instantiation	167, 417, 192, 331, 127, 332, 402, 130, 163, 164	⊢
	: , : , : , : , : , :
104	instantiation	225, 331, 426, 332, 128, 129, 402, 130, 163, 164, 131*	⊢
	: , : , : , : , : , :
105	instantiation	165, 132, 188	⊢
	: , :
106	instantiation	167, 331, 426, 417, 332, 133, 402, 283, 188	⊢
	: , : , : , : , : , :
107	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
108	instantiation	424, 374, 134	⊢
	: , : , :
109	instantiation	337, 135	,  ⊢
	: , : , :
110	instantiation	363, 136, 137	⊢
	: , : , :
111	instantiation	424, 377, 138	⊢
	: , : , :
112	instantiation	165, 166, 139	⊢
	: , :
113	instantiation	363, 140, 141	⊢
	: , : , :
114	instantiation	320, 190, 215	⊢
	: , :
115	instantiation	167, 331, 426, 417, 332, 191, 402, 340, 195	⊢
	: , : , : , : , : , :
116	instantiation	337, 142	⊢
	: , : , :
117	theorem		⊢
	proveit.trigonometry.sine_pos_interval
118	instantiation	143, 252, 358, 144, 145	,  ⊢
	: , : , :
119	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
120	theorem		⊢
	proveit.numbers.ordering.relax_less
121	instantiation	167, 417, 426, 331, 146, 332, 402, 340, 227	⊢
	: , : , : , : , : , :
122	instantiation	363, 147, 148	⊢
	: , : , :
123	instantiation	181, 178	⊢
	:
124	instantiation	320, 366, 296	⊢
	: , :
125	instantiation	214	⊢
	: , : , :
126	instantiation	355, 152, 382, 149*	⊢
	: , :
127	instantiation	214	⊢
	: , : , :
128	instantiation	399	⊢
	: , :
129	instantiation	399	⊢
	: , :
130	instantiation	150, 318, 349, 350	⊢
	: , :
131	instantiation	151, 402, 318, 177, 152, 153*, 154*	⊢
	: , : , : , :
132	instantiation	424, 410, 155	⊢
	: , : , :
133	instantiation	399	⊢
	: , :
134	instantiation	424, 395, 156	⊢
	: , : , :
135	instantiation	157, 158, 159, 402, 283, 188, 298, 381, 284, 160, 338*, 285*	,  ⊢
	: , : , :
136	instantiation	167, 417, 192, 331, 162, 332, 318, 341, 163, 164	⊢
	: , : , : , : , : , :
137	instantiation	161, 331, 192, 332, 162, 341, 163, 164	⊢
	: , : , : , :
138	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
139	instantiation	165, 194, 195	⊢
	: , :
140	instantiation	167, 417, 426, 331, 168, 332, 166, 194, 195	⊢
	: , : , : , : , : , :
141	instantiation	167, 331, 426, 332, 191, 168, 402, 340, 194, 195	⊢
	: , : , : , : , : , :
142	instantiation	363, 169, 170	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
144	instantiation	171, 252, 219, 217	,  ⊢
	: , : , :
145	instantiation	172, 173, 174	,  ⊢
	: , :
146	instantiation	399	⊢
	: , :
147	instantiation	337, 175	⊢
	: , : , :
148	instantiation	209, 176, 177, 178, 179*	⊢
	: , : , :
149	instantiation	376, 349	⊢
	:
150	theorem		⊢
	proveit.numbers.division.div_complex_closure
151	theorem		⊢
	proveit.numbers.division.prod_of_fracs
152	instantiation	424, 374, 180	⊢
	: , : , :
153	instantiation	181, 402	⊢
	:
154	instantiation	363, 182, 183	⊢
	: , : , :
155	instantiation	320, 411, 296	⊢
	: , :
156	instantiation	424, 407, 184	⊢
	: , : , :
157	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_products
158	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
159	instantiation	214	⊢
	: , : , :
160	instantiation	185, 186	,  ⊢
	:
161	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
162	instantiation	214	⊢
	: , : , :
163	instantiation	424, 410, 322	⊢
	: , : , :
164	instantiation	187, 188, 189	⊢
	: , :
165	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
166	instantiation	424, 410, 190	⊢
	: , : , :
167	theorem		⊢
	proveit.numbers.multiplication.disassociation
168	instantiation	399	⊢
	: , :
169	instantiation	224, 331, 426, 417, 332, 191, 402, 340, 194, 195	⊢
	: , : , : , : , : , : , :
170	instantiation	225, 417, 192, 331, 193, 332, 194, 402, 340, 195	⊢
	: , : , : , : , : , :
171	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
172	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
173	instantiation	196, 252, 219, 217	,  ⊢
	: , : , :
174	instantiation	197, 198, 199	,  ⊢
	: , : , :
175	instantiation	363, 200, 201	⊢
	: , : , :
176	instantiation	424, 374, 202	⊢
	: , : , :
177	instantiation	424, 374, 203	⊢
	: , : , :
178	instantiation	424, 410, 204	⊢
	: , : , :
179	instantiation	401, 340	⊢
	:
180	instantiation	424, 395, 205	⊢
	: , : , :
181	theorem		⊢
	proveit.numbers.division.frac_one_denom
182	instantiation	384, 426, 206, 207, 388, 208	⊢
	: , : , : , :
183	instantiation	209, 356, 318, 388*, 347*	⊢
	: , : , :
184	instantiation	424, 415, 315	⊢
	: , : , :
185	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_if_in_complex_nonzero
186	instantiation	210, 211, 212	,  ⊢
	: , : , :
187	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
188	instantiation	424, 410, 213	⊢
	: , : , :
189	instantiation	424, 410, 298	⊢
	: , : , :
190	instantiation	320, 411, 358	⊢
	: , :
191	instantiation	399	⊢
	: , :
192	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
193	instantiation	214	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
195	instantiation	424, 410, 215	⊢
	: , : , :
196	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
197	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
198	instantiation	216, 252, 219, 217	,  ⊢
	: , : , :
199	instantiation	218, 219, 220, 291, 221, 222*, 223*	⊢
	: , : , :
200	instantiation	224, 331, 417, 332, 402, 340, 227	⊢
	: , : , : , : , : , : , :
201	instantiation	225, 417, 426, 331, 226, 332, 340, 402, 227	⊢
	: , : , : , : , : , :
202	instantiation	424, 248, 378	⊢
	: , : , :
203	instantiation	424, 395, 228	⊢
	: , : , :
204	instantiation	320, 411, 246	⊢
	: , :
205	instantiation	424, 407, 229	⊢
	: , : , :
206	instantiation	399	⊢
	: , :
207	instantiation	399	⊢
	: , :
208	instantiation	400, 349	⊢
	:
209	theorem		⊢
	proveit.numbers.division.frac_cancel_left
210	theorem		⊢
	proveit.logic.equality.sub_right_side_into
211	instantiation	424, 374, 230	,  ⊢
	: , : , :
212	instantiation	337, 231	⊢
	: , : , :
213	instantiation	424, 262, 232	⊢
	: , : , :
214	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
215	instantiation	233, 234, 235	⊢
	: , :
216	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
217	instantiation	236, 371, 314	,  ⊢
	:
218	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
219	instantiation	379, 358, 411, 381	⊢
	: , :
220	instantiation	320, 306, 252	⊢
	: , :
221	instantiation	237, 306, 252, 358, 238, 239	⊢
	: , : , :
222	instantiation	240, 241, 242, 243	⊢
	: , : , : , :
223	instantiation	363, 244, 245	⊢
	: , : , :
224	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
225	theorem		⊢
	proveit.numbers.multiplication.association
226	instantiation	399	⊢
	: , :
227	instantiation	424, 410, 246	⊢
	: , : , :
228	instantiation	424, 407, 247	⊢
	: , : , :
229	instantiation	424, 415, 367	⊢
	: , : , :
230	instantiation	424, 248, 249	,  ⊢
	: , : , :
231	instantiation	337, 250	⊢
	: , : , :
232	instantiation	278, 251	⊢
	:
233	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
234	instantiation	309, 252, 380, 253	⊢
	: , : , :
235	instantiation	328, 321	⊢
	:
236	theorem		⊢
	proveit.physics.quantum.QPE._scaled_abs_delta_b_floor_diff_interval
237	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
238	instantiation	254, 378	⊢
	:
239	instantiation	255, 343	⊢
	:
240	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
241	instantiation	363, 256, 257	⊢
	: , : , :
242	instantiation	258	⊢
	:
243	instantiation	259, 290	⊢
	: , :
244	instantiation	337, 290	⊢
	: , : , :
245	instantiation	259, 260, 261*	⊢
	: , :
246	instantiation	424, 262, 263	⊢
	: , : , :
247	instantiation	424, 415, 382	⊢
	: , : , :
248	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
249	instantiation	264, 265	,  ⊢
	:
250	instantiation	337, 266	⊢
	: , : , :
251	instantiation	267, 268, 269	⊢
	: , :
252	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
253	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
254	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
255	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
256	instantiation	363, 270, 271	⊢
	: , : , :
257	instantiation	272, 273	⊢
	:
258	axiom		⊢
	proveit.logic.equality.equals_reflexivity
259	theorem		⊢
	proveit.logic.equality.equals_reversal
260	instantiation	274, 331, 426, 417, 332, 275, 341, 340	⊢
	: , : , : , : , : , :
261	instantiation	363, 276, 277	⊢
	: , : , :
262	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
263	instantiation	278, 280	⊢
	:
264	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
265	instantiation	279, 280, 281	,  ⊢
	:
266	instantiation	304, 282, 283, 284, 285*	⊢
	: , :
267	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
268	instantiation	424, 410, 286	⊢
	: , : , :
269	instantiation	287, 288	⊢
	:
270	instantiation	337, 289	⊢
	: , : , :
271	instantiation	337, 290	⊢
	: , : , :
272	theorem		⊢
	proveit.numbers.addition.elim_zero_left
273	instantiation	424, 410, 291	⊢
	: , : , :
274	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
275	instantiation	399	⊢
	: , :
276	instantiation	337, 292	⊢
	: , : , :
277	instantiation	400, 340	⊢
	:
278	theorem		⊢
	proveit.numbers.absolute_value.abs_complex_closure
279	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
280	instantiation	424, 410, 293	⊢
	: , : , :
281	instantiation	294, 295	,  ⊢
	: , :
282	instantiation	424, 410, 321	⊢
	: , : , :
283	instantiation	424, 410, 296	⊢
	: , : , :
284	instantiation	398, 315	⊢
	:
285	instantiation	297, 402, 351, 298, 381, 299*	⊢
	: , : , :
286	instantiation	300, 301	⊢
	:
287	theorem		⊢
	proveit.numbers.negation.complex_closure
288	instantiation	424, 410, 302	⊢
	: , : , :
289	instantiation	303, 341	⊢
	:
290	instantiation	304, 340, 402, 381, 305*	⊢
	: , :
291	instantiation	320, 306, 358	⊢
	: , :
292	instantiation	307, 409, 423, 308*	⊢
	: , : , : , :
293	instantiation	309, 310, 359, 311	⊢
	: , : , :
294	theorem		⊢
	proveit.numbers.addition.subtraction.nonzero_difference_if_different
295	instantiation	312, 313, 352, 314	,  ⊢
	: , :
296	instantiation	368, 369, 315	⊢
	: , : , :
297	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
298	instantiation	424, 418, 316	⊢
	: , : , :
299	instantiation	317, 334, 318, 319*	⊢
	: , :
300	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
301	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
302	instantiation	320, 321, 322	⊢
	: , :
303	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
304	theorem		⊢
	proveit.numbers.division.div_as_mult
305	instantiation	363, 323, 324	⊢
	: , : , :
306	instantiation	424, 418, 325	⊢
	: , : , :
307	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
308	instantiation	363, 326, 327	⊢
	: , : , :
309	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
310	instantiation	328, 359	⊢
	:
311	instantiation	329, 371	⊢
	:
312	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_not_eq_scaledNonzeroInt
313	instantiation	330, 331, 417, 332	⊢
	: , : , : , : , :
314	assumption		⊢
315	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
316	instantiation	424, 422, 333	⊢
	: , : , :
317	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
318	instantiation	424, 410, 380	⊢
	: , : , :
319	instantiation	401, 334	⊢
	:
320	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
321	instantiation	424, 418, 335	⊢
	: , : , :
322	instantiation	424, 418, 336	⊢
	: , : , :
323	instantiation	337, 338	⊢
	: , : , :
324	instantiation	339, 340, 341	⊢
	: , :
325	instantiation	424, 342, 343	⊢
	: , : , :
326	instantiation	384, 426, 344, 345, 346, 347	⊢
	: , : , : , :
327	instantiation	348, 349, 350	⊢
	:
328	theorem		⊢
	proveit.numbers.negation.real_closure
329	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_floor_diff_in_interval
330	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
331	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
332	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
333	instantiation	413, 409	⊢
	:
334	instantiation	424, 410, 351	⊢
	: , : , :
335	instantiation	424, 422, 352	⊢
	: , : , :
336	instantiation	424, 353, 354	⊢
	: , : , :
337	axiom		⊢
	proveit.logic.equality.substitution
338	instantiation	355, 356, 382, 357*	⊢
	: , :
339	theorem		⊢
	proveit.numbers.multiplication.commutation
340	instantiation	424, 410, 358	⊢
	: , : , :
341	instantiation	424, 410, 359	⊢
	: , : , :
342	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
343	instantiation	360, 361, 362	⊢
	: , :
344	instantiation	399	⊢
	: , :
345	instantiation	399	⊢
	: , :
346	instantiation	363, 364, 365	⊢
	: , : , :
347	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
348	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
349	instantiation	424, 410, 366	⊢
	: , : , :
350	instantiation	398, 367	⊢
	:
351	instantiation	368, 369, 406	⊢
	: , : , :
352	instantiation	424, 370, 371	⊢
	: , : , :
353	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
354	instantiation	372, 396, 373	⊢
	: , :
355	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
356	instantiation	424, 374, 375	⊢
	: , : , :
357	instantiation	376, 402	⊢
	:
358	instantiation	424, 377, 378	⊢
	: , : , :
359	instantiation	379, 380, 411, 381	⊢
	: , :
360	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
361	instantiation	424, 383, 382	⊢
	: , : , :
362	instantiation	424, 383, 416	⊢
	: , : , :
363	axiom		⊢
	proveit.logic.equality.equals_transitivity
364	instantiation	384, 426, 385, 386, 387, 388	⊢
	: , : , : , :
365	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
366	instantiation	424, 418, 389	⊢
	: , : , :
367	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
368	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
369	instantiation	390, 391	⊢
	: , :
370	instantiation	392, 393, 414	⊢
	: , :
371	assumption		⊢
372	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
373	instantiation	413, 394	⊢
	:
374	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
375	instantiation	424, 395, 396	⊢
	: , : , :
376	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
377	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
378	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
379	theorem		⊢
	proveit.numbers.division.div_real_closure
380	instantiation	424, 418, 397	⊢
	: , : , :
381	instantiation	398, 416	⊢
	:
382	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
383	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
384	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
385	instantiation	399	⊢
	: , :
386	instantiation	399	⊢
	: , :
387	instantiation	400, 402	⊢
	:
388	instantiation	401, 402	⊢
	:
389	instantiation	424, 422, 403	⊢
	: , : , :
390	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
391	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
392	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
393	instantiation	404, 405, 409	⊢
	: , :
394	instantiation	424, 420, 406	⊢
	: , : , :
395	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
396	instantiation	424, 407, 408	⊢
	: , : , :
397	instantiation	424, 422, 409	⊢
	: , : , :
398	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
399	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
400	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
401	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
402	instantiation	424, 410, 411	⊢
	: , : , :
403	instantiation	424, 425, 412	⊢
	: , : , :
404	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
405	instantiation	413, 414	⊢
	:
406	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
407	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
408	instantiation	424, 415, 416	⊢
	: , : , :
409	instantiation	424, 425, 417	⊢
	: , : , :
410	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
411	instantiation	424, 418, 419	⊢
	: , : , :
412	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
413	theorem		⊢
	proveit.numbers.negation.int_closure
414	instantiation	424, 420, 421	⊢
	: , : , :
415	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
416	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
417	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
418	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
419	instantiation	424, 422, 423	⊢
	: , : , :
420	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
421	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
422	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
423	instantiation	424, 425, 426	⊢
	: , : , :
424	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
425	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
426	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements