Show the Proof

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

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