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