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