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