Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

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