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