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