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.physics.quantum.circuits.equiv_transitivity
2	modus ponens	4, 5	⊢
3	instantiation	6, 7	⊢
	: , :
4	instantiation	16, 697, 709, 650, 17, 651	⊢
	: , : , : , : , : , : , : , :
5	instantiation	631, 8, 9	⊢
	: , : , :
6	theorem		⊢
	proveit.physics.quantum.circuits.equiv_reversal
7	modus ponens	10, 11	⊢
8	instantiation	631, 12, 13	⊢
	: , : , :
9	instantiation	197, 430, 30, 14, 15	⊢
	: , : , : , :
10	instantiation	16, 697, 709, 650, 17, 651	⊢
	: , : , : , : , : , : , : , :
11	instantiation	44, 615, 18, 712, 424, 19, 20, 262, 21, 22, 23, 24, 25, 229, 502, 650, 430, 58, 26, 514*	⊢
	: , : , : , : , : , :
12	instantiation	631, 27, 28	⊢
	: , : , :
13	instantiation	197, 430, 29, 30, 31	⊢
	: , : , : , :
14	instantiation	32, 430	⊢
	: , :
15	instantiation	353, 704, 286, 287, 288, 289*	⊢
	: , : , : , : , : , :
16	theorem		⊢
	proveit.physics.quantum.circuits.circuit_equiv_temporal_sub
17	instantiation	665	⊢
	: , :
18	instantiation	665	⊢
	: , :
19	instantiation	665	⊢
	: , :
20	instantiation	33, 34	⊢
	: , :
21	instantiation	562, 35, 36, 37	⊢
	: , : , : , :
22	instantiation	572, 38	⊢
	: , :
23	instantiation	665	⊢
	: , :
24	instantiation	572, 39	⊢
	: , :
25	instantiation	562, 40, 538, 41	⊢
	: , : , : , :
26	instantiation	141, 635, 42, 144, 43, 146	⊢
	: , :
27	instantiation	44, 392, 45, 613, 46, 424, 47, 48, 49, 262, 50, 51, 52, 53, 54, 55, 56, 229, 129, 650, 57, 58, 59, 514, 60, 61*, 62*, 63*	⊢
	: , : , : , : , : , :
28	instantiation	197, 430, 64, 65, 66	⊢
	: , : , : , :
29	instantiation	562, 67, 612, 319	⊢
	: , : , : , :
30	instantiation	562, 68, 612, 319	⊢
	: , : , : , :
31	instantiation	252, 253, 254, 402*	⊢
	: , : , : , :
32	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
33	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
34	instantiation	69, 712	⊢
	:
35	instantiation	70	⊢
	: , : , :
36	instantiation	630	⊢
	:
37	instantiation	572, 71	⊢
	: , :
38	instantiation	173, 72, 514	⊢
	: , : , :
39	instantiation	227, 72, 502	⊢
	: , : , :
40	instantiation	73	⊢
	: , :
41	instantiation	572, 74	⊢
	: , :
42	instantiation	655	⊢
	: , : , :
43	instantiation	572, 404	⊢
	: , :
44	theorem		⊢
	proveit.physics.quantum.circuits.output_consolidation
45	instantiation	562, 75, 91, 86	⊢
	: , : , : , :
46	instantiation	316, 691, 702, 613, 248	⊢
	: , : , :
47	instantiation	562, 76, 91, 86	⊢
	: , : , : , :
48	instantiation	369, 77, 167	⊢
	: , : , :
49	modus ponens	78, 79	⊢
50	instantiation	562, 80, 81, 82	⊢
	: , : , : , :
51	instantiation	572, 83	⊢
	: , :
52	instantiation	572, 84	⊢
	: , :
53	instantiation	562, 85, 91, 86	⊢
	: , : , : , :
54	instantiation	572, 87	⊢
	: , :
55	instantiation	618, 88, 89	⊢
	: , : , :
56	instantiation	562, 90, 91, 92	⊢
	: , : , : , :
57	modus ponens	93, 94	⊢
58	instantiation	348, 430, 374	⊢
	: , :
59	instantiation	95, 697, 344, 709, 96, 491, 97, 98	⊢
	: , : , : , : , : , :
60	instantiation	618, 99, 100	,  ⊢
	: , : , :
61	instantiation	618, 101, 102	⊢
	: , : , :
62	instantiation	618, 103, 104	⊢
	: , : , :
63	instantiation	618, 105, 106	,  ⊢
	: , : , :
64	instantiation	562, 107, 612, 319	⊢
	: , : , : , :
65	instantiation	562, 108, 612, 319	⊢
	: , : , : , :
66	instantiation	252, 253, 254	⊢
	: , : , : , :
67	instantiation	309, 615, 109, 311, 312, 313, 344, 314*	⊢
	: , : , : , :
68	instantiation	631, 110, 376	⊢
	: , : , :
69	theorem		⊢
	proveit.physics.quantum.QPE._psi_t_ket_is_normalized_vec
70	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3
71	instantiation	631, 111, 112	⊢
	: , : , :
72	instantiation	348, 697, 339	⊢
	: , :
73	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2
74	instantiation	631, 113, 114	⊢
	: , : , :
75	instantiation	309, 132, 115, 134, 135, 313, 344, 136*	⊢
	: , : , : , :
76	instantiation	309, 132, 116, 134, 135, 313, 344, 136*	⊢
	: , : , : , :
77	instantiation	369, 117, 118	⊢
	: , : , :
78	instantiation	378, 691, 702, 248	⊢
	: , : , : , :
79	generalization	119	⊢
80	instantiation	309, 132, 120, 121, 135, 313, 426, 122*	⊢
	: , : , : , :
81	instantiation	642, 673, 623	⊢
	: , :
82	instantiation	572, 123	⊢
	: , :
83	instantiation	173, 128, 514	⊢
	: , : , :
84	instantiation	197, 430, 180, 124, 125	⊢
	: , : , : , :
85	instantiation	309, 132, 126, 134, 135, 313, 344, 136*	⊢
	: , : , : , :
86	instantiation	572, 127	⊢
	: , :
87	instantiation	227, 128, 129	⊢
	: , : , :
88	instantiation	572, 130	⊢
	: , :
89	instantiation	572, 131	⊢
	: , :
90	instantiation	309, 132, 133, 134, 135, 313, 344, 136*	⊢
	: , : , : , :
91	instantiation	630	⊢
	:
92	instantiation	572, 137	⊢
	: , :
93	instantiation	378, 701, 702, 379	⊢
	: , : , : , :
94	generalization	138	⊢
95	theorem		⊢
	proveit.logic.booleans.conjunction.disassociate
96	instantiation	665	⊢
	: , :
97	instantiation	562, 139, 445, 140	⊢
	: , : , : , :
98	instantiation	141, 142, 143, 144, 476, 145, 146	⊢
	: , :
99	instantiation	560, 147	,  ⊢
	: , : , :
100	instantiation	618, 148, 149	,  ⊢
	: , : , :
101	instantiation	560, 150	⊢
	: , : , :
102	instantiation	572, 151	⊢
	: , :
103	instantiation	560, 152	⊢
	: , : , :
104	instantiation	154, 613	⊢
	: , :
105	instantiation	560, 153	,  ⊢
	: , : , :
106	instantiation	154, 155	,  ⊢
	: , :
107	instantiation	309, 615, 156, 311, 312, 313, 344, 314*	⊢
	: , : , : , :
108	instantiation	631, 157, 376	⊢
	: , : , :
109	instantiation	665	⊢
	: , :
110	instantiation	425, 426	⊢
	: , : , :
111	instantiation	425, 158	⊢
	: , : , :
112	instantiation	618, 159, 160	⊢
	: , : , :
113	instantiation	425, 161	⊢
	: , : , :
114	instantiation	618, 162, 163	⊢
	: , : , :
115	instantiation	655	⊢
	: , : , :
116	instantiation	655	⊢
	: , : , :
117	instantiation	518, 519, 433, 164	⊢
	: , : , : , :
118	instantiation	560, 165	⊢
	: , : , :
119	instantiation	369, 166, 167	,  ⊢
	: , : , :
120	instantiation	655	⊢
	: , : , :
121	instantiation	655	⊢
	: , : , :
122	instantiation	618, 168, 169	⊢
	: , : , :
123	instantiation	631, 170, 171	⊢
	: , : , :
124	instantiation	562, 172, 612, 319	⊢
	: , : , : , :
125	instantiation	173, 253, 360, 402*	⊢
	: , : , :
126	instantiation	655	⊢
	: , : , :
127	instantiation	429, 338	⊢
	: , :
128	instantiation	405, 174, 175	⊢
	:
129	instantiation	618, 176, 177	⊢
	: , : , :
130	instantiation	197, 430, 181, 178, 179	⊢
	: , : , : , :
131	instantiation	197, 430, 180, 181, 182	⊢
	: , : , : , :
132	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
133	instantiation	655	⊢
	: , : , :
134	instantiation	655	⊢
	: , : , :
135	instantiation	655	⊢
	: , : , :
136	instantiation	618, 183, 184	⊢
	: , : , :
137	instantiation	631, 185, 186	⊢
	: , : , :
138	instantiation	405, 187, 188	,  ⊢
	:
139	instantiation	631, 189, 491	⊢
	: , : , :
140	instantiation	572, 190	⊢
	: , :
141	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
142	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
143	instantiation	191	⊢
	: , : , : , :
144	instantiation	630	⊢
	:
145	modus ponens	192, 193	⊢
146	instantiation	630	⊢
	:
147	instantiation	566, 709, 650, 651, 196, 607, 623	,  ⊢
	: , : , : , : , : , : , :
148	instantiation	604, 650, 635, 709, 651, 194, 196, 623, 607, 643	,  ⊢
	: , : , : , : , : , :
149	instantiation	575, 697, 650, 195, 651, 196, 623, 643	,  ⊢
	: , : , : , : , : , : , : , :
150	instantiation	197, 430, 198, 260, 199	⊢
	: , : , : , :
151	instantiation	560, 200, 201*	⊢
	: , : , :
152	instantiation	560, 514	⊢
	: , : , :
153	instantiation	560, 307	,  ⊢
	: , : , :
154	theorem		⊢
	proveit.physics.quantum.circuits.unary_multi_output_reduction
155	instantiation	202, 203, 204	,  ⊢
	:
156	instantiation	665	⊢
	: , :
157	instantiation	425, 426	⊢
	: , : , :
158	instantiation	466, 635, 205, 697, 339, 709	⊢
	: , :
159	instantiation	560, 444	⊢
	: , : , :
160	instantiation	598, 650, 697, 709, 651, 206, 673, 595, 643, 207*	⊢
	: , : , : , : , : , :
161	instantiation	466, 635, 208, 709, 339	⊢
	: , :
162	instantiation	560, 444	⊢
	: , : , :
163	instantiation	598, 650, 697, 709, 651, 312, 643, 595, 209*	⊢
	: , : , : , : , : , :
164	instantiation	480, 519, 481, 210	⊢
	: , : , : , :
165	instantiation	560, 211	⊢
	: , : , :
166	instantiation	518, 519, 433, 212	,  ⊢
	: , : , : , :
167	instantiation	560, 213	⊢
	: , : , :
168	instantiation	418, 635, 214, 215, 421, 376	⊢
	: , : , : , :
169	instantiation	618, 216, 217	⊢
	: , : , :
170	instantiation	425, 218	⊢
	: , : , :
171	instantiation	618, 219, 220	⊢
	: , : , :
172	instantiation	309, 615, 221, 311, 312, 313, 344, 314*	⊢
	: , : , : , :
173	theorem		⊢
	proveit.core_expr_types.tuples.partition_front
174	instantiation	703, 222, 223	⊢
	: , :
175	instantiation	457, 224	⊢
	: , :
176	instantiation	604, 650, 697, 709, 651, 341, 623, 643, 607	⊢
	: , : , : , : , : , :
177	instantiation	225, 643, 623, 578	⊢
	: , : , :
178	instantiation	562, 226, 612, 319	⊢
	: , : , : , :
179	instantiation	227, 228, 229, 230*	⊢
	: , : , :
180	instantiation	560, 231	⊢
	: , : , :
181	instantiation	560, 232	⊢
	: , : , :
182	instantiation	353, 671, 286, 233, 234, 235*	⊢
	: , : , : , : , : , :
183	instantiation	418, 635, 236, 237, 421, 491	⊢
	: , : , : , :
184	instantiation	618, 238, 239	⊢
	: , : , :
185	instantiation	425, 240	⊢
	: , : , :
186	instantiation	618, 241, 242	⊢
	: , : , :
187	instantiation	703, 696, 707	,  ⊢
	: , :
188	instantiation	581, 627, 503, 243, 244, 245*, 246*	,  ⊢
	: , : , :
189	instantiation	425, 344	⊢
	: , : , :
190	instantiation	429, 247	⊢
	: , :
191	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
192	instantiation	378, 691, 702, 248	⊢
	: , : , : , :
193	generalization	249	⊢
194	instantiation	655	⊢
	: , : , :
195	instantiation	665	⊢
	: , :
196	instantiation	710, 689, 250	,  ⊢
	: , : , :
197	theorem		⊢
	proveit.core_expr_types.operations.operands_substitution_via_tuple
198	instantiation	562, 251, 612, 319	⊢
	: , : , : , :
199	instantiation	252, 253, 254	⊢
	: , : , : , :
200	instantiation	255, 712	⊢
	:
201	instantiation	256, 650, 426, 709, 651, 376, 257, 258, 259, 260, 261, 262	⊢
	: , : , : , : , : , : , : , : , : , :
202	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
203	instantiation	703, 681, 707	,  ⊢
	: , :
204	instantiation	263, 436, 601, 264, 265, 266*, 267*	,  ⊢
	: , : , :
205	instantiation	655	⊢
	: , : , :
206	instantiation	665	⊢
	: , :
207	instantiation	618, 268, 269	⊢
	: , : , :
208	instantiation	655	⊢
	: , : , :
209	instantiation	618, 270, 641	⊢
	: , : , :
210	instantiation	518, 519, 271, 521	⊢
	: , : , : , :
211	instantiation	560, 272	⊢
	: , : , :
212	instantiation	480, 519, 481, 273	,  ⊢
	: , : , : , :
213	instantiation	274, 673	⊢
	:
214	instantiation	655	⊢
	: , : , :
215	instantiation	655	⊢
	: , : , :
216	instantiation	566, 709, 650, 651, 643, 623	⊢
	: , : , : , : , : , : , :
217	instantiation	598, 650, 697, 709, 651, 567, 643, 623, 641*	⊢
	: , : , : , : , : , :
218	instantiation	710, 472, 275	⊢
	: , : , :
219	instantiation	560, 444	⊢
	: , : , :
220	instantiation	562, 276, 277, 278	⊢
	: , : , : , :
221	instantiation	665	⊢
	: , :
222	instantiation	710, 711, 392	⊢
	: , : , :
223	instantiation	657, 279, 394	⊢
	: , : , :
224	instantiation	533, 280	⊢
	: , :
225	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
226	instantiation	281, 282, 283*	⊢
	: , : , : , :
227	theorem		⊢
	proveit.core_expr_types.tuples.partition_back
228	instantiation	405, 284, 285	⊢
	:
229	instantiation	542, 595, 643, 514	⊢
	: , : , :
230	instantiation	602, 643, 623, 578	⊢
	: , : , :
231	instantiation	353, 704, 286, 287, 288, 289*	⊢
	: , : , : , : , : , :
232	instantiation	618, 290, 291	⊢
	: , : , :
233	instantiation	572, 292	⊢
	: , :
234	instantiation	572, 293	⊢
	: , :
235	instantiation	604, 650, 697, 709, 651, 294, 295, 607, 623	,  ⊢
	: , : , : , : , : , :
236	instantiation	655	⊢
	: , : , :
237	instantiation	655	⊢
	: , : , :
238	instantiation	604, 709, 697, 606, 643, 623, 607	⊢
	: , : , : , : , : , :
239	instantiation	576, 650, 709, 651, 643, 623, 578	⊢
	: , : , : , : , : , : , : , :
240	instantiation	466, 635, 296, 430, 339, 709	⊢
	: , :
241	instantiation	560, 444	⊢
	: , : , :
242	instantiation	596, 709, 623, 643	⊢
	: , : , : , :
243	instantiation	483, 690, 677	,  ⊢
	: , :
244	instantiation	297, 503, 690, 677, 298, 299	,  ⊢
	: , : , :
245	instantiation	562, 300, 301, 302	⊢
	: , : , : , :
246	instantiation	562, 303, 304, 305	,  ⊢
	: , : , : , :
247	instantiation	405, 659, 306	⊢
	:
248	instantiation	581, 503, 677, 639, 582, 399*, 432*	⊢
	: , : , :
249	instantiation	572, 307	,  ⊢
	: , :
250	instantiation	710, 692, 308	,  ⊢
	: , : , :
251	instantiation	309, 615, 310, 311, 312, 313, 344, 314*	⊢
	: , : , : , :
252	theorem		⊢
	proveit.core_expr_types.tuples.merge_front
253	instantiation	348, 650, 468	⊢
	: , :
254	instantiation	572, 360	⊢
	: , :
255	axiom		⊢
	proveit.physics.quantum.QPE._psi_t_def
256	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_disassociation
257	instantiation	562, 315, 612, 319	⊢
	: , : , : , :
258	instantiation	316, 701, 702, 519, 379	⊢
	: , : , :
259	instantiation	555, 317	⊢
	:
260	instantiation	562, 318, 612, 319	⊢
	: , : , : , :
261	modus ponens	320, 321	⊢
262	axiom		⊢
	proveit.physics.quantum.QPE._u_ket_register
263	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
264	instantiation	710, 692, 322	,  ⊢
	: , : , :
265	instantiation	323, 601, 656, 682, 324, 325	,  ⊢
	: , : , :
266	instantiation	562, 326, 327, 328	⊢
	: , : , : , :
267	instantiation	562, 329, 330, 331	,  ⊢
	: , : , : , :
268	instantiation	560, 332	⊢
	: , : , :
269	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
270	instantiation	560, 333	⊢
	: , : , :
271	instantiation	672, 556, 334	⊢
	: , :
272	instantiation	560, 335	⊢
	: , : , :
273	instantiation	518, 519, 336, 521	,  ⊢
	: , : , : , :
274	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
275	instantiation	451, 697, 650, 337, 651, 338, 339, 709, 452	⊢
	: , : , : , : , :
276	instantiation	604, 650, 697, 651, 341, 340, 623, 643, 595	⊢
	: , : , : , : , : , :
277	instantiation	596, 697, 709, 341, 623, 643	⊢
	: , : , : , :
278	instantiation	598, 709, 697, 650, 567, 651, 623, 643, 641*	⊢
	: , : , : , : , : , :
279	instantiation	669, 342	⊢
	: , :
280	instantiation	569, 392	⊢
	:
281	theorem		⊢
	proveit.core_expr_types.tuples.extended_range_len
282	instantiation	343, 344	⊢
	: , : , :
283	instantiation	618, 345, 346	⊢
	: , : , :
284	instantiation	703, 705, 456	⊢
	: , :
285	instantiation	457, 347	⊢
	: , :
286	instantiation	348, 349, 468	⊢
	: , :
287	instantiation	572, 350	⊢
	: , :
288	instantiation	572, 351	⊢
	: , :
289	instantiation	618, 352, 547	,  ⊢
	: , : , :
290	instantiation	353, 701, 354, 355, 356	⊢
	: , : , : , : , : , :
291	modus ponens	357, 358	⊢
292	instantiation	618, 359, 360	⊢
	: , : , :
293	instantiation	618, 361, 514	⊢
	: , : , :
294	instantiation	665	⊢
	: , :
295	instantiation	710, 689, 362	,  ⊢
	: , : , :
296	instantiation	655	⊢
	: , : , :
297	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right
298	instantiation	382, 701, 702, 699	,  ⊢
	: , : , :
299	instantiation	363, 709	⊢
	:
300	instantiation	604, 650, 697, 709, 651, 550, 610, 643, 603	⊢
	: , : , : , : , : , :
301	instantiation	604, 697, 650, 550, 606, 651, 610, 643, 623, 607	⊢
	: , : , : , : , : , :
302	instantiation	618, 364, 384	⊢
	: , : , :
303	instantiation	604, 650, 697, 709, 651, 365, 684, 643, 603	,  ⊢
	: , : , : , : , : , :
304	instantiation	604, 697, 650, 365, 606, 651, 684, 643, 623, 607	,  ⊢
	: , : , : , : , : , :
305	instantiation	576, 709, 650, 651, 684, 643, 623, 578	,  ⊢
	: , : , : , : , : , : , : , :
306	instantiation	457, 582	⊢
	: , :
307	instantiation	618, 366, 367	,  ⊢
	: , : , :
308	instantiation	710, 695, 368	,  ⊢
	: , : , :
309	theorem		⊢
	proveit.core_expr_types.tuples.general_len
310	instantiation	665	⊢
	: , :
311	instantiation	665	⊢
	: , :
312	instantiation	665	⊢
	: , :
313	instantiation	369, 709, 421	⊢
	: , : , :
314	instantiation	618, 370, 371	⊢
	: , : , :
315	instantiation	631, 372, 376	⊢
	: , : , :
316	theorem		⊢
	proveit.logic.booleans.conjunction.redundant_conjunction_general
317	instantiation	373, 697, 374	⊢
	: , :
318	instantiation	631, 375, 376	⊢
	: , : , :
319	instantiation	572, 377	⊢
	: , :
320	instantiation	378, 701, 702, 379	⊢
	: , : , : , :
321	generalization	380	⊢
322	instantiation	710, 695, 381	,  ⊢
	: , : , :
323	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
324	instantiation	382, 691, 702, 687	,  ⊢
	: , : , :
325	instantiation	569, 615	⊢
	:
326	instantiation	604, 650, 697, 709, 651, 605, 610, 673, 385	⊢
	: , : , : , : , : , :
327	instantiation	604, 697, 650, 605, 594, 651, 610, 673, 623, 644	⊢
	: , : , : , : , : , :
328	instantiation	618, 383, 384	⊢
	: , : , :
329	instantiation	604, 650, 697, 709, 651, 386, 638, 673, 385	,  ⊢
	: , : , : , : , : , :
330	instantiation	604, 697, 650, 386, 594, 651, 638, 673, 623, 644	,  ⊢
	: , : , : , : , : , :
331	instantiation	576, 709, 650, 651, 638, 673, 623, 538	,  ⊢
	: , : , : , : , : , : , : , :
332	instantiation	387, 673	⊢
	:
333	instantiation	387, 643	⊢
	:
334	instantiation	631, 388, 389	⊢
	: , : , :
335	instantiation	560, 390	⊢
	: , : , :
336	instantiation	672, 556, 391	,  ⊢
	: , :
337	instantiation	665	⊢
	: , :
338	instantiation	710, 472, 392	⊢
	: , : , :
339	instantiation	657, 393, 394	⊢
	: , : , :
340	instantiation	665	⊢
	: , :
341	instantiation	665	⊢
	: , :
342	theorem		⊢
	proveit.numbers.number_sets.integers.zero_set_within_int
343	theorem		⊢
	proveit.core_expr_types.tuples.range_len_is_nat
344	instantiation	631, 468, 395	⊢
	: , : , :
345	instantiation	560, 561	⊢
	: , : , :
346	instantiation	562, 396, 397, 398	⊢
	: , : , : , :
347	instantiation	581, 503, 677, 639, 582, 399*, 475*	⊢
	: , : , :
348	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
349	instantiation	710, 472, 400	⊢
	: , : , :
350	instantiation	618, 401, 402	⊢
	: , : , :
351	instantiation	618, 403, 404	⊢
	: , : , :
352	instantiation	604, 650, 697, 709, 651, 577, 580, 610, 623	,  ⊢
	: , : , : , : , : , :
353	theorem		⊢
	proveit.core_expr_types.tuples.shift_equivalence
354	instantiation	405, 406, 407	⊢
	:
355	instantiation	572, 408	⊢
	: , :
356	instantiation	572, 409	⊢
	: , :
357	instantiation	410, 705, 707	⊢
	: , : , : , : , :
358	generalization	411	⊢
359	instantiation	560, 414	⊢
	: , : , :
360	instantiation	618, 412, 413	⊢
	: , : , :
361	instantiation	560, 414	⊢
	: , : , :
362	instantiation	710, 692, 415	,  ⊢
	: , : , :
363	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
364	instantiation	576, 709, 650, 651, 610, 643, 623, 578	⊢
	: , : , : , : , : , : , : , :
365	instantiation	665	⊢
	: , :
366	instantiation	604, 650, 635, 709, 651, 416, 638, 607, 623, 643	,  ⊢
	: , : , : , : , : , :
367	instantiation	575, 709, 650, 651, 638, 643, 623	,  ⊢
	: , : , : , : , : , : , : , :
368	instantiation	710, 686, 417	,  ⊢
	: , : , :
369	theorem		⊢
	proveit.logic.equality.sub_left_side_into
370	instantiation	418, 697, 419, 420, 421, 491	⊢
	: , : , : , :
371	instantiation	618, 422, 423	⊢
	: , : , :
372	instantiation	425, 426	⊢
	: , : , :
373	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
374	instantiation	710, 472, 424	⊢
	: , : , :
375	instantiation	425, 426	⊢
	: , : , :
376	instantiation	618, 427, 428	⊢
	: , : , :
377	instantiation	429, 430	⊢
	: , :
378	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
379	instantiation	581, 503, 676, 639, 497, 431*, 432*	⊢
	: , : , :
380	instantiation	518, 519, 433, 434	,  ⊢
	: , : , : , :
381	instantiation	703, 681, 694	,  ⊢
	: , :
382	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
383	instantiation	576, 709, 650, 651, 610, 673, 623, 538	⊢
	: , : , : , : , : , : , : , :
384	instantiation	435, 623, 612	⊢
	: , :
385	instantiation	710, 689, 436	⊢
	: , : , :
386	instantiation	665	⊢
	: , :
387	theorem		⊢
	proveit.numbers.addition.elim_zero_right
388	instantiation	662, 634, 437	⊢
	: , :
389	instantiation	618, 438, 439	⊢
	: , : , :
390	instantiation	560, 500	⊢
	: , : , :
391	instantiation	631, 440, 441	,  ⊢
	: , : , :
392	instantiation	532, 712, 613	⊢
	: , :
393	instantiation	669, 442	⊢
	: , :
394	instantiation	443, 444	⊢
	: , :
395	instantiation	562, 500, 445, 446	⊢
	: , : , : , :
396	instantiation	604, 709, 697, 594, 595, 623, 644, 673	⊢
	: , : , : , : , : , :
397	instantiation	596, 650, 635, 651, 447, 623, 644, 673	⊢
	: , : , : , :
398	instantiation	579, 673, 623, 538	⊢
	: , : , :
399	instantiation	562, 448, 449, 450	⊢
	: , : , : , :
400	instantiation	451, 709, 650, 651, 452	⊢
	: , : , : , : , :
401	instantiation	560, 593	⊢
	: , : , :
402	instantiation	618, 453, 454	⊢
	: , : , :
403	instantiation	560, 593	⊢
	: , : , :
404	instantiation	551, 623	⊢
	:
405	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
406	instantiation	703, 455, 456	⊢
	: , :
407	instantiation	457, 458	⊢
	: , :
408	instantiation	618, 459, 460	⊢
	: , : , :
409	instantiation	542, 623, 461, 643, 475	⊢
	: , : , :
410	theorem		⊢
	proveit.core_expr_types.tuples.range_fn_transformation
411	instantiation	618, 462, 463	,  ⊢
	: , : , :
412	instantiation	604, 650, 697, 709, 651, 550, 610, 643	⊢
	: , : , : , : , : , :
413	instantiation	598, 709, 697, 650, 567, 651, 610, 643, 641*	⊢
	: , : , : , : , : , :
414	instantiation	622, 643	⊢
	:
415	instantiation	710, 695, 464	,  ⊢
	: , : , :
416	instantiation	655	⊢
	: , : , :
417	assumption		⊢
418	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
419	instantiation	665	⊢
	: , :
420	instantiation	665	⊢
	: , :
421	instantiation	602, 643, 578	⊢
	: , : , :
422	instantiation	604, 709, 697, 650, 606, 651, 643, 623, 607	⊢
	: , : , : , : , : , :
423	instantiation	465, 643, 623, 578	⊢
	: , : , :
424	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
425	theorem		⊢
	proveit.core_expr_types.tuples.range_len
426	instantiation	466, 635, 467, 650, 468, 709	⊢
	: , :
427	instantiation	560, 500	⊢
	: , : , :
428	instantiation	562, 469, 470, 471	⊢
	: , : , : , :
429	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
430	instantiation	710, 472, 712	⊢
	: , : , :
431	instantiation	618, 473, 474	⊢
	: , : , :
432	instantiation	562, 475, 578, 476	⊢
	: , : , : , :
433	instantiation	477, 643, 478, 479	⊢
	: , :
434	instantiation	480, 519, 481, 482	,  ⊢
	: , : , : , :
435	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_reverse
436	instantiation	483, 639, 484	⊢
	: , :
437	instantiation	631, 485, 486	⊢
	: , : , :
438	instantiation	649, 709, 635, 650, 487, 651, 634, 663, 558, 653	⊢
	: , : , : , : , : , :
439	instantiation	649, 650, 697, 635, 651, 636, 487, 673, 654, 663, 558, 653	⊢
	: , : , : , : , : , :
440	instantiation	662, 634, 488	,  ⊢
	: , :
441	instantiation	618, 489, 490	,  ⊢
	: , : , :
442	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.zero_set_within_nat
443	theorem		⊢
	proveit.logic.sets.enumeration.fold_singleton
444	theorem		⊢
	proveit.numbers.negation.negated_zero
445	instantiation	630	⊢
	:
446	instantiation	572, 491	⊢
	: , :
447	instantiation	655	⊢
	: , : , :
448	instantiation	618, 492, 493	⊢
	: , : , :
449	instantiation	542, 568, 623, 673, 494	⊢
	: , : , :
450	instantiation	630	⊢
	:
451	theorem		⊢
	proveit.numbers.addition.add_nat_pos_from_nonneg
452	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
453	instantiation	604, 650, 697, 709, 651, 550, 610, 643, 623	⊢
	: , : , : , : , : , :
454	instantiation	495, 623, 643, 612	⊢
	: , : , :
455	instantiation	710, 711, 496	⊢
	: , : , :
456	instantiation	706, 691	⊢
	:
457	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
458	instantiation	581, 601, 676, 639, 497, 498*, 499*	⊢
	: , : , :
459	instantiation	560, 500	⊢
	: , : , :
460	instantiation	618, 501, 502	⊢
	: , : , :
461	instantiation	710, 689, 503	⊢
	: , : , :
462	instantiation	560, 504	,  ⊢
	: , : , :
463	instantiation	618, 505, 506	,  ⊢
	: , : , :
464	instantiation	710, 507, 508	,  ⊢
	: , : , :
465	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
466	theorem		⊢
	proveit.numbers.addition.add_nat_closure
467	instantiation	655	⊢
	: , : , :
468	instantiation	509, 510	⊢
	:
469	instantiation	604, 709, 697, 606, 595, 623, 607, 643	⊢
	: , : , : , : , : , :
470	instantiation	596, 650, 635, 651, 511, 623, 607, 643	⊢
	: , : , : , :
471	instantiation	579, 643, 623, 578	⊢
	: , : , :
472	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
473	instantiation	604, 709, 697, 650, 550, 651, 595, 610, 643	⊢
	: , : , : , : , : , :
474	instantiation	596, 650, 697, 651, 550, 610, 643	⊢
	: , : , : , :
475	instantiation	618, 512, 513	⊢
	: , : , :
476	instantiation	572, 514	⊢
	: , :
477	theorem		⊢
	proveit.numbers.division.div_complex_closure
478	instantiation	515, 673	⊢
	:
479	instantiation	516, 554, 517	⊢
	: , :
480	theorem		⊢
	proveit.linear_algebra.addition.binary_closure
481	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
482	instantiation	518, 519, 520, 521	,  ⊢
	: , : , : , :
483	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
484	instantiation	522, 682	⊢
	:
485	instantiation	662, 523, 653	⊢
	: , :
486	instantiation	649, 650, 697, 709, 651, 524, 663, 558, 653	⊢
	: , : , : , : , : , :
487	instantiation	655	⊢
	: , : , :
488	instantiation	631, 525, 526	,  ⊢
	: , : , :
489	instantiation	649, 709, 635, 650, 637, 651, 634, 663, 591, 653	,  ⊢
	: , : , : , : , : , :
490	instantiation	649, 650, 697, 635, 651, 636, 637, 673, 654, 663, 591, 653	,  ⊢
	: , : , : , : , : , :
491	instantiation	618, 527, 528	⊢
	: , : , :
492	instantiation	604, 709, 697, 650, 550, 651, 643, 610	⊢
	: , : , : , : , : , :
493	instantiation	618, 529, 530	⊢
	: , : , :
494	instantiation	631, 537, 531	⊢
	: , : , :
495	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_31
496	instantiation	532, 613	⊢
	: , :
497	instantiation	533, 534	⊢
	: , :
498	instantiation	618, 535, 536	⊢
	: , : , :
499	instantiation	562, 537, 538, 539	⊢
	: , : , : , :
500	instantiation	592, 610, 643, 593*	⊢
	: , :
501	instantiation	618, 540, 541	⊢
	: , : , :
502	instantiation	542, 643, 673, 641	⊢
	: , : , :
503	instantiation	710, 692, 543	⊢
	: , : , :
504	instantiation	604, 709, 697, 650, 550, 651, 580, 610, 643	,  ⊢
	: , : , : , : , : , :
505	instantiation	604, 650, 635, 697, 651, 544, 545, 580, 610, 643, 607, 623	,  ⊢
	: , : , : , : , : , :
506	instantiation	618, 546, 547	,  ⊢
	: , : , :
507	instantiation	700, 691, 705	⊢
	: , :
508	assumption		⊢
509	theorem		⊢
	proveit.numbers.negation.nat_closure
510	instantiation	548, 701, 549	⊢
	:
511	instantiation	655	⊢
	: , : , :
512	instantiation	604, 709, 697, 650, 550, 651, 623, 610, 643	⊢
	: , : , : , : , : , :
513	instantiation	602, 623, 643, 612	⊢
	: , : , :
514	instantiation	551, 643	⊢
	:
515	theorem		⊢
	proveit.numbers.exponentiation.sqrt_complex_closure
516	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
517	instantiation	552, 553, 554	⊢
	: , :
518	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
519	instantiation	555, 615	⊢
	:
520	instantiation	672, 556, 557	,  ⊢
	: , :
521	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
522	theorem		⊢
	proveit.numbers.negation.real_closure
523	instantiation	662, 663, 558	⊢
	: , :
524	instantiation	665	⊢
	: , :
525	instantiation	662, 559, 653	,  ⊢
	: , :
526	instantiation	649, 650, 697, 709, 651, 652, 663, 591, 653	,  ⊢
	: , : , : , : , : , :
527	instantiation	560, 561	⊢
	: , : , :
528	instantiation	562, 563, 564, 565	⊢
	: , : , : , :
529	instantiation	566, 709, 650, 651, 643, 610	⊢
	: , : , : , : , : , : , :
530	instantiation	598, 650, 697, 709, 651, 567, 643, 610, 641*	⊢
	: , : , : , : , : , :
531	instantiation	642, 623, 568	⊢
	: , :
532	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
533	theorem		⊢
	proveit.numbers.ordering.relax_less
534	instantiation	569, 712	⊢
	:
535	instantiation	604, 709, 697, 650, 605, 651, 595, 610, 673	⊢
	: , : , : , : , : , :
536	instantiation	596, 650, 697, 651, 605, 610, 673	⊢
	: , : , : , :
537	instantiation	618, 570, 571	⊢
	: , : , :
538	instantiation	630	⊢
	:
539	instantiation	572, 641	⊢
	: , :
540	instantiation	618, 573, 574	⊢
	: , : , :
541	instantiation	575, 650, 709, 651, 623, 673, 607	⊢
	: , : , : , : , : , : , : , :
542	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
543	instantiation	710, 695, 701	⊢
	: , : , :
544	instantiation	655	⊢
	: , : , :
545	instantiation	665	⊢
	: , :
546	instantiation	576, 697, 650, 709, 577, 651, 580, 610, 643, 623, 578	,  ⊢
	: , : , : , : , : , : , : , :
547	instantiation	579, 623, 580, 612	,  ⊢
	: , : , :
548	theorem		⊢
	proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
549	instantiation	581, 629, 677, 639, 582, 583*, 584*	⊢
	: , : , :
550	instantiation	665	⊢
	: , :
551	theorem		⊢
	proveit.numbers.addition.elim_zero_left
552	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
553	instantiation	710, 586, 585	⊢
	: , : , :
554	instantiation	710, 586, 587	⊢
	: , : , :
555	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
556	instantiation	710, 689, 588	⊢
	: , : , :
557	instantiation	631, 589, 590	,  ⊢
	: , : , :
558	instantiation	672, 673, 603	⊢
	: , :
559	instantiation	662, 663, 591	,  ⊢
	: , :
560	axiom		⊢
	proveit.logic.equality.substitution
561	instantiation	592, 610, 673, 593*	⊢
	: , :
562	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
563	instantiation	604, 709, 697, 594, 595, 623, 644, 643	⊢
	: , : , : , : , : , :
564	instantiation	596, 650, 635, 651, 597, 623, 644, 643	⊢
	: , : , : , :
565	instantiation	598, 709, 697, 650, 599, 651, 623, 644, 643, 600*	⊢
	: , : , : , : , : , :
566	theorem		⊢
	proveit.numbers.addition.leftward_commutation
567	instantiation	665	⊢
	: , :
568	instantiation	710, 689, 601	⊢
	: , : , :
569	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
570	instantiation	604, 709, 697, 650, 605, 651, 623, 610, 673	⊢
	: , : , : , : , : , :
571	instantiation	602, 623, 673, 612	⊢
	: , : , :
572	theorem		⊢
	proveit.logic.equality.equals_reversal
573	instantiation	604, 650, 697, 709, 651, 605, 610, 673, 603	⊢
	: , : , : , : , : , :
574	instantiation	604, 697, 650, 605, 606, 651, 610, 673, 623, 607	⊢
	: , : , : , : , : , :
575	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
576	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
577	instantiation	665	⊢
	: , :
578	instantiation	630	⊢
	:
579	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
580	instantiation	710, 689, 608	,  ⊢
	: , : , :
581	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
582	instantiation	609, 712	⊢
	:
583	instantiation	642, 643, 610	⊢
	: , :
584	instantiation	611, 623, 612	⊢
	: , :
585	instantiation	710, 614, 613	⊢
	: , : , :
586	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
587	instantiation	710, 614, 615	⊢
	: , : , :
588	instantiation	710, 679, 616	⊢
	: , : , :
589	instantiation	662, 634, 617	,  ⊢
	: , :
590	instantiation	618, 619, 620	,  ⊢
	: , : , :
591	instantiation	672, 673, 621	,  ⊢
	: , :
592	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
593	instantiation	622, 623	⊢
	:
594	instantiation	665	⊢
	: , :
595	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
596	theorem		⊢
	proveit.numbers.addition.elim_zero_any
597	instantiation	655	⊢
	: , : , :
598	theorem		⊢
	proveit.numbers.addition.association
599	instantiation	665	⊢
	: , :
600	instantiation	631, 624, 625	⊢
	: , : , :
601	instantiation	710, 692, 626	⊢
	: , : , :
602	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
603	instantiation	710, 689, 627	⊢
	: , : , :
604	theorem		⊢
	proveit.numbers.addition.disassociation
605	instantiation	665	⊢
	: , :
606	instantiation	665	⊢
	: , :
607	instantiation	683, 643	⊢
	:
608	instantiation	710, 692, 628	,  ⊢
	: , : , :
609	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
610	instantiation	710, 689, 629	⊢
	: , : , :
611	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
612	instantiation	630	⊢
	:
613	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
614	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
615	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
616	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
617	instantiation	631, 632, 633	,  ⊢
	: , : , :
618	axiom		⊢
	proveit.logic.equality.equals_transitivity
619	instantiation	649, 709, 635, 650, 637, 651, 634, 663, 664, 653	,  ⊢
	: , : , : , : , : , :
620	instantiation	649, 650, 697, 635, 651, 636, 637, 673, 654, 663, 664, 653	,  ⊢
	: , : , : , : , : , :
621	instantiation	683, 638	,  ⊢
	:
622	theorem		⊢
	proveit.numbers.negation.double_negation
623	instantiation	710, 689, 639	⊢
	: , : , :
624	instantiation	640, 643, 673, 641	⊢
	: , : , :
625	instantiation	642, 643, 644	⊢
	: , :
626	instantiation	710, 695, 691	⊢
	: , : , :
627	instantiation	710, 692, 645	⊢
	: , : , :
628	instantiation	710, 695, 646	,  ⊢
	: , : , :
629	instantiation	710, 692, 647	⊢
	: , : , :
630	axiom		⊢
	proveit.logic.equality.equals_reflexivity
631	theorem		⊢
	proveit.logic.equality.sub_right_side_into
632	instantiation	662, 648, 653	,  ⊢
	: , :
633	instantiation	649, 650, 697, 709, 651, 652, 663, 664, 653	,  ⊢
	: , : , : , : , : , :
634	instantiation	662, 673, 654	⊢
	: , :
635	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
636	instantiation	665	⊢
	: , :
637	instantiation	655	⊢
	: , : , :
638	instantiation	710, 689, 656	,  ⊢
	: , : , :
639	instantiation	657, 658, 712	⊢
	: , : , :
640	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
641	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
642	theorem		⊢
	proveit.numbers.addition.commutation
643	instantiation	710, 689, 677	⊢
	: , : , :
644	instantiation	683, 673	⊢
	:
645	instantiation	710, 695, 659	⊢
	: , : , :
646	instantiation	710, 660, 661	,  ⊢
	: , : , :
647	instantiation	710, 695, 704	⊢
	: , : , :
648	instantiation	662, 663, 664	,  ⊢
	: , :
649	theorem		⊢
	proveit.numbers.multiplication.disassociation
650	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
651	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
652	instantiation	665	⊢
	: , :
653	instantiation	710, 689, 666	⊢
	: , : , :
654	instantiation	710, 689, 667	⊢
	: , : , :
655	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
656	instantiation	710, 692, 668	,  ⊢
	: , : , :
657	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
658	instantiation	669, 670	⊢
	: , :
659	instantiation	703, 707, 671	⊢
	: , :
660	instantiation	700, 705, 707	⊢
	: , :
661	assumption		⊢
662	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
663	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
664	instantiation	672, 673, 674	,  ⊢
	: , :
665	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
666	instantiation	675, 676, 677, 678	⊢
	: , : , :
667	instantiation	710, 679, 680	⊢
	: , : , :
668	instantiation	710, 695, 681	,  ⊢
	: , : , :
669	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
670	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
671	instantiation	706, 705	⊢
	:
672	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
673	instantiation	710, 689, 682	⊢
	: , : , :
674	instantiation	683, 684	,  ⊢
	:
675	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
676	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
677	instantiation	710, 692, 685	⊢
	: , : , :
678	axiom		⊢
	proveit.physics.quantum.QPE._phase_in_interval
679	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
680	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
681	instantiation	710, 686, 687	,  ⊢
	: , : , :
682	instantiation	710, 692, 688	⊢
	: , : , :
683	theorem		⊢
	proveit.numbers.negation.complex_closure
684	instantiation	710, 689, 690	,  ⊢
	: , : , :
685	instantiation	710, 695, 705	⊢
	: , : , :
686	instantiation	700, 691, 702	⊢
	: , :
687	assumption		⊢
688	instantiation	710, 695, 694	⊢
	: , : , :
689	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
690	instantiation	710, 692, 693	,  ⊢
	: , : , :
691	instantiation	703, 704, 694	⊢
	: , :
692	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
693	instantiation	710, 695, 696	,  ⊢
	: , : , :
694	instantiation	710, 708, 697	⊢
	: , : , :
695	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
696	instantiation	710, 698, 699	,  ⊢
	: , : , :
697	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
698	instantiation	700, 701, 702	⊢
	: , :
699	assumption		⊢
700	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
701	instantiation	703, 704, 705	⊢
	: , :
702	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
703	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
704	instantiation	706, 707	⊢
	:
705	instantiation	710, 708, 709	⊢
	: , : , :
706	theorem		⊢
	proveit.numbers.negation.int_closure
707	instantiation	710, 711, 712	⊢
	: , : , :
708	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
709	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
710	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
711	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
712	assumption		⊢
*equality replacement requirements