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