Show the Proof

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

	step type	requirements	statement
0	instantiation	1, 2	⊢
	: , :
1	reference	100	⊢
2	instantiation	27, 3, 4, 5	⊢
	: , : , : , :
3	instantiation	214, 6, 7, 8*	⊢
	: , : , :
4	instantiation	227, 9	⊢
	: , : , :
5	instantiation	193	⊢
	:
6	instantiation	17, 25, 223, 274, 225, 43, 58, 22, 10	⊢
	: , : , : , : , : , : , : , : , : , :
7	instantiation	227, 11	⊢
	: , : , :
8	instantiation	12, 13, 14, 25, 26, 15*	⊢
	: , : , : , : , :
9	instantiation	100, 16	⊢
	: , :
10	instantiation	57, 58, 26, 23	⊢
	: , : , : , :
11	instantiation	17, 26, 274, 223, 225, 43, 58, 22, 23	⊢
	: , : , : , : , : , : , : , : , : , :
12	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled
13	instantiation	18, 283, 20, 43, 58	⊢
	: , : , :
14	instantiation	19, 283, 20, 43, 58, 21, 22, 23	⊢
	: , : , : , :
15	instantiation	24, 25, 26	⊢
	: , :
16	instantiation	27, 28, 29, 30	⊢
	: , : , : , :
17	theorem		⊢
	proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
18	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
19	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
20	instantiation	237	⊢
	: , :
21	instantiation	237	⊢
	: , :
22	instantiation	31, 43, 32, 33	⊢
	: , : , : , :
23	modus ponens	34, 35	⊢
24	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
25	instantiation	98, 236, 36, 37	⊢
	: , :
26	instantiation	98, 236, 38, 39	⊢
	: , :
27	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
28	instantiation	214, 40, 41	⊢
	: , : , :
29	instantiation	193	⊢
	:
30	instantiation	100, 42	⊢
	: , :
31	theorem		⊢
	proveit.linear_algebra.addition.binary_closure
32	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
33	instantiation	57, 43, 44, 45	⊢
	: , : , : , :
34	instantiation	46, 281, 58	⊢
	: , : , : , : , : , :
35	generalization	47	⊢
36	instantiation	167, 254, 48	⊢
	: , :
37	instantiation	49, 106, 104	⊢
	: , : , :
38	instantiation	167, 254, 80	⊢
	: , :
39	instantiation	49, 110, 108	⊢
	: , : , :
40	instantiation	227, 50	⊢
	: , : , :
41	instantiation	202, 236, 51, 52, 53*	⊢
	: , :
42	instantiation	214, 54, 55	⊢
	: , : , :
43	instantiation	75, 283	⊢
	:
44	instantiation	167, 77, 56	⊢
	: , :
45	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
46	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
47	instantiation	57, 58, 59, 60	,  ⊢
	: , : , : , :
48	instantiation	234, 61, 62	⊢
	: , :
49	theorem		⊢
	proveit.logic.equality.sub_left_side_into
50	instantiation	214, 63, 64	⊢
	: , : , :
51	instantiation	169, 105, 109	⊢
	: , :
52	instantiation	65, 286, 66, 67, 68	⊢
	: , :
53	instantiation	214, 69, 70	⊢
	: , : , :
54	instantiation	227, 71	⊢
	: , : , :
55	instantiation	227, 72	⊢
	: , : , :
56	instantiation	133, 73, 74	⊢
	: , : , :
57	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
58	instantiation	75, 76	⊢
	:
59	instantiation	167, 77, 78	,  ⊢
	: , :
60	instantiation	79, 258, 210	,  ⊢
	: , :
61	instantiation	98, 221, 254, 203	⊢
	: , :
62	instantiation	206, 80	⊢
	:
63	instantiation	227, 174	⊢
	: , : , :
64	instantiation	214, 81, 82	⊢
	: , : , :
65	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
66	instantiation	237	⊢
	: , :
67	instantiation	83, 105, 106	⊢
	:
68	instantiation	83, 109, 110	⊢
	:
69	instantiation	227, 84	⊢
	: , : , :
70	instantiation	214, 85, 86	⊢
	: , : , :
71	instantiation	214, 87, 88	⊢
	: , : , :
72	instantiation	214, 89, 90	⊢
	: , : , :
73	instantiation	169, 136, 91	⊢
	: , :
74	instantiation	214, 92, 93	⊢
	: , : , :
75	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
76	instantiation	94, 286, 246	⊢
	: , :
77	instantiation	284, 263, 95	⊢
	: , : , :
78	instantiation	133, 96, 97	,  ⊢
	: , : , :
79	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_in_register_space
80	instantiation	98, 235, 254, 203	⊢
	: , :
81	instantiation	227, 99	⊢
	: , : , :
82	instantiation	100, 101	⊢
	: , :
83	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
84	instantiation	102, 105, 109, 165, 106, 110, 145*, 148*	⊢
	: , : , :
85	instantiation	195, 274, 286, 223, 103, 225, 236, 146, 150	⊢
	: , : , : , : , : , :
86	instantiation	207, 223, 286, 225, 103, 146, 150	⊢
	: , : , : , :
87	instantiation	227, 104	⊢
	: , : , :
88	instantiation	202, 236, 105, 106, 107*	⊢
	: , :
89	instantiation	227, 108	⊢
	: , : , :
90	instantiation	202, 236, 109, 110, 111*	⊢
	: , :
91	instantiation	133, 112, 113	⊢
	: , : , :
92	instantiation	195, 274, 137, 223, 114, 225, 136, 170, 171, 132	⊢
	: , : , : , : , : , :
93	instantiation	195, 223, 286, 137, 225, 138, 114, 254, 155, 170, 171, 132	⊢
	: , : , : , : , : , :
94	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
95	instantiation	284, 188, 115	⊢
	: , : , :
96	instantiation	169, 136, 116	,  ⊢
	: , :
97	instantiation	214, 117, 118	,  ⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.division.div_complex_closure
99	instantiation	119, 192, 239	⊢
	: , :
100	theorem		⊢
	proveit.logic.equality.equals_reversal
101	instantiation	120, 254, 121, 122	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
103	instantiation	237	⊢
	: , :
104	instantiation	227, 123	⊢
	: , : , :
105	instantiation	124, 254	⊢
	:
106	instantiation	128, 262, 125	⊢
	: , :
107	instantiation	214, 126, 127	⊢
	: , : , :
108	instantiation	227, 191	⊢
	: , : , :
109	instantiation	167, 254, 192	⊢
	: , :
110	instantiation	128, 262, 129	⊢
	: , :
111	instantiation	214, 130, 131	⊢
	: , : , :
112	instantiation	169, 152, 132	⊢
	: , :
113	instantiation	195, 223, 286, 274, 225, 153, 170, 171, 132	⊢
	: , : , : , : , : , :
114	instantiation	156	⊢
	: , : , :
115	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
116	instantiation	133, 134, 135	,  ⊢
	: , : , :
117	instantiation	195, 274, 137, 223, 139, 225, 136, 170, 171, 154	,  ⊢
	: , : , : , : , : , :
118	instantiation	195, 223, 286, 137, 225, 138, 139, 254, 155, 170, 171, 154	,  ⊢
	: , : , : , : , : , :
119	theorem		⊢
	proveit.numbers.addition.commutation
120	theorem		⊢
	proveit.numbers.exponentiation.product_of_pos_powers
121	instantiation	284, 140, 269	⊢
	: , : , :
122	instantiation	284, 140, 230	⊢
	: , : , :
123	instantiation	214, 141, 142	⊢
	: , : , :
124	theorem		⊢
	proveit.numbers.exponentiation.sqrt_complex_closure
125	instantiation	143, 144, 262	⊢
	: , :
126	instantiation	227, 145	⊢
	: , : , :
127	instantiation	149, 146	⊢
	:
128	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
129	instantiation	284, 147, 230	⊢
	: , : , :
130	instantiation	227, 148	⊢
	: , : , :
131	instantiation	149, 150	⊢
	:
132	instantiation	284, 263, 151	⊢
	: , : , :
133	theorem		⊢
	proveit.logic.equality.sub_right_side_into
134	instantiation	169, 152, 154	,  ⊢
	: , :
135	instantiation	195, 223, 286, 274, 225, 153, 170, 171, 154	,  ⊢
	: , : , : , : , : , :
136	instantiation	169, 254, 155	⊢
	: , :
137	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
138	instantiation	237	⊢
	: , :
139	instantiation	156	⊢
	: , : , :
140	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
141	instantiation	214, 157, 158	⊢
	: , : , :
142	instantiation	214, 159, 160	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
144	instantiation	284, 270, 161	⊢
	: , : , :
145	instantiation	164, 254, 250, 165, 203, 162*	⊢
	: , : , :
146	instantiation	167, 254, 163	⊢
	: , :
147	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
148	instantiation	164, 254, 205, 165, 203, 166*	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
150	instantiation	167, 254, 178	⊢
	: , :
151	instantiation	284, 272, 168	⊢
	: , : , :
152	instantiation	169, 170, 171	⊢
	: , :
153	instantiation	237	⊢
	: , :
154	instantiation	284, 263, 172	,  ⊢
	: , : , :
155	instantiation	284, 263, 173	⊢
	: , : , :
156	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
157	instantiation	227, 174	⊢
	: , : , :
158	instantiation	227, 175	⊢
	: , : , :
159	instantiation	176, 223, 286, 274, 225, 177, 192, 239, 178	⊢
	: , : , : , : , : , :
160	instantiation	179, 192, 239, 180	⊢
	: , : , :
161	instantiation	284, 278, 281	⊢
	: , : , :
162	instantiation	181, 239, 236, 226*	⊢
	: , :
163	instantiation	284, 263, 182	⊢
	: , : , :
164	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
165	instantiation	284, 272, 183	⊢
	: , : , :
166	instantiation	214, 184, 185	⊢
	: , : , :
167	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
168	instantiation	284, 279, 232	⊢
	: , : , :
169	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
170	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
171	instantiation	284, 263, 186	⊢
	: , : , :
172	instantiation	284, 272, 187	,  ⊢
	: , : , :
173	instantiation	284, 188, 189	⊢
	: , : , :
174	instantiation	202, 221, 254, 203, 190*	⊢
	: , :
175	instantiation	227, 191	⊢
	: , : , :
176	theorem		⊢
	proveit.numbers.addition.disassociation
177	instantiation	237	⊢
	: , :
178	instantiation	206, 192	⊢
	:
179	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
180	instantiation	193	⊢
	:
181	theorem		⊢
	proveit.numbers.negation.pos_times_neg
182	instantiation	194, 250	⊢
	:
183	instantiation	284, 279, 233	⊢
	: , : , :
184	instantiation	195, 223, 286, 274, 225, 208, 239, 235, 196	⊢
	: , : , : , : , : , :
185	instantiation	197, 286, 223, 208, 225, 239, 235, 236, 198*	⊢
	: , : , : , : , :
186	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
187	instantiation	284, 279, 199	,  ⊢
	: , : , :
188	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
189	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
190	instantiation	214, 200, 201	⊢
	: , : , :
191	instantiation	202, 235, 254, 203, 204*	⊢
	: , :
192	instantiation	284, 263, 205	⊢
	: , : , :
193	axiom		⊢
	proveit.logic.equality.equals_reflexivity
194	theorem		⊢
	proveit.numbers.negation.real_closure
195	theorem		⊢
	proveit.numbers.multiplication.disassociation
196	instantiation	206, 236	⊢
	:
197	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
198	instantiation	207, 286, 223, 208, 225, 239, 235	⊢
	: , : , : , :
199	instantiation	284, 209, 210	,  ⊢
	: , : , :
200	instantiation	227, 228	⊢
	: , : , :
201	instantiation	214, 211, 212	⊢
	: , : , :
202	theorem		⊢
	proveit.numbers.division.div_as_mult
203	instantiation	213, 283	⊢
	:
204	instantiation	214, 215, 216	⊢
	: , : , :
205	instantiation	284, 272, 217	⊢
	: , : , :
206	theorem		⊢
	proveit.numbers.negation.complex_closure
207	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
208	instantiation	237	⊢
	: , :
209	instantiation	218, 219, 220	⊢
	: , :
210	assumption		⊢
211	instantiation	229, 221, 239	⊢
	: , :
212	instantiation	222, 274, 286, 223, 224, 225, 239, 235, 236, 226*	⊢
	: , : , : , : , : , :
213	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
214	axiom		⊢
	proveit.logic.equality.equals_transitivity
215	instantiation	227, 228	⊢
	: , : , :
216	instantiation	229, 235, 239	⊢
	: , :
217	instantiation	284, 268, 230	⊢
	: , : , :
218	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
219	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
220	instantiation	231, 232, 233	⊢
	: , :
221	instantiation	234, 235, 236	⊢
	: , :
222	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
223	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
224	instantiation	237	⊢
	: , :
225	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
226	instantiation	238, 239	⊢
	:
227	axiom		⊢
	proveit.logic.equality.substitution
228	instantiation	240, 241, 281, 242*	⊢
	: , :
229	theorem		⊢
	proveit.numbers.multiplication.commutation
230	instantiation	243, 269, 244	⊢
	: , :
231	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
232	instantiation	245, 280, 246	⊢
	: , :
233	instantiation	247, 267	⊢
	:
234	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
235	instantiation	284, 263, 248	⊢
	: , : , :
236	instantiation	284, 263, 249	⊢
	: , : , :
237	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
238	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
239	instantiation	284, 263, 250	⊢
	: , : , :
240	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
241	instantiation	284, 251, 252	⊢
	: , : , :
242	instantiation	253, 254	⊢
	:
243	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
244	instantiation	284, 282, 258	⊢
	: , : , :
245	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
246	instantiation	284, 255, 258	⊢
	: , : , :
247	theorem		⊢
	proveit.numbers.negation.int_closure
248	instantiation	256, 257, 258	⊢
	: , : , :
249	instantiation	284, 272, 259	⊢
	: , : , :
250	instantiation	284, 272, 260	⊢
	: , : , :
251	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
252	instantiation	284, 261, 262	⊢
	: , : , :
253	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
254	instantiation	284, 263, 264	⊢
	: , : , :
255	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
256	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
257	instantiation	265, 266	⊢
	: , :
258	assumption		⊢
259	instantiation	284, 279, 267	⊢
	: , : , :
260	instantiation	284, 268, 269	⊢
	: , : , :
261	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
262	instantiation	284, 270, 271	⊢
	: , : , :
263	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
264	instantiation	284, 272, 273	⊢
	: , : , :
265	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
266	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
267	instantiation	284, 285, 274	⊢
	: , : , :
268	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
269	instantiation	275, 276, 277	⊢
	: , :
270	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
271	instantiation	284, 278, 283	⊢
	: , : , :
272	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
273	instantiation	284, 279, 280	⊢
	: , : , :
274	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
275	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
276	instantiation	284, 282, 281	⊢
	: , : , :
277	instantiation	284, 282, 283	⊢
	: , : , :
278	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
279	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
280	instantiation	284, 285, 286	⊢
	: , : , :
281	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
282	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
283	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
284	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
285	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
286	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements