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	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_eq
2	instantiation	5, 3, 4	⊢
	: , :
3	instantiation	5, 6, 7	⊢
	: , :
4	instantiation	147, 8, 9*, 10*, 11*	⊢
	: , : , :
5	theorem		⊢
	proveit.logic.equality.rhs_via_equality
6	instantiation	201, 12, 13	⊢
	: , : , :
7	instantiation	147, 14, 15*, 16*, 17*	⊢
	: , : , :
8	modus ponens	18, 19	⊢
9	instantiation	78, 235	⊢
	: , :
10	instantiation	78, 235	⊢
	: , :
11	instantiation	151, 20	⊢
	: , :
12	instantiation	21, 237, 238, 26, 22, 23, 24*	⊢
	: , : , : , : , :
13	instantiation	25, 240, 26, 142, 27*, 28*, 29*	⊢
	: , : , : , : , :
14	modus ponens	30, 31	⊢
15	instantiation	78, 235	⊢
	: , :
16	instantiation	78, 235	⊢
	: , :
17	instantiation	32, 33, 34, 35	⊢
	: , : , : , :
18	instantiation	102, 123	⊢
	: , : , : , : , : , : , :
19	generalization	36	⊢
20	modus ponens	37, 38	⊢
21	theorem		⊢
	proveit.linear_algebra.addition.vec_sum_split_after
22	instantiation	39, 40	⊢
	: , :
23	instantiation	41, 42, 43, 200, 44, 45*, 46*	⊢
	: , : , :
24	instantiation	197, 47, 48	⊢
	: , : , :
25	theorem		⊢
	proveit.linear_algebra.addition.vec_sum_index_shift
26	instantiation	239, 141, 241	⊢
	: , :
27	instantiation	49, 193, 50	⊢
	: , :
28	instantiation	197, 51, 52	⊢
	: , : , :
29	instantiation	53, 193	⊢
	:
30	instantiation	102, 123	⊢
	: , : , : , : , : , : , :
31	generalization	54	⊢
32	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
33	instantiation	147, 55, 56*, 57*	⊢
	: , : , :
34	instantiation	151, 58	⊢
	: , :
35	instantiation	147, 59	⊢
	: , : , :
36	instantiation	60, 249, 235	,  ⊢
	: , :
37	instantiation	122, 252, 123, 211, 156, 212	⊢
	: , : , : , : , : , : , : , : , : , : , :
38	generalization	61	⊢
39	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
40	instantiation	62, 187	⊢
	:
41	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
42	instantiation	250, 228, 63	⊢
	: , : , :
43	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
44	instantiation	64, 187	⊢
	:
45	instantiation	197, 65, 66	⊢
	: , : , :
46	instantiation	197, 67, 68	⊢
	: , : , :
47	instantiation	87, 211, 247, 252, 212, 88, 193, 146, 164	⊢
	: , : , : , : , : , :
48	instantiation	69, 164, 193, 70	⊢
	: , : , :
49	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
50	instantiation	91	⊢
	:
51	instantiation	87, 211, 247, 252, 212, 71, 95, 146, 96	⊢
	: , : , : , : , : , :
52	instantiation	197, 72, 73	⊢
	: , : , :
53	theorem		⊢
	proveit.numbers.negation.double_negation
54	instantiation	201, 74, 75	,  ⊢
	: , : , :
55	modus ponens	76, 77	⊢
56	instantiation	78, 235	⊢
	: , :
57	instantiation	78, 235	⊢
	: , :
58	modus ponens	79, 80	⊢
59	instantiation	151, 81	⊢
	: , :
60	theorem		⊢
	proveit.physics.quantum.algebra.prepend_num_ket_with_zero_ket
61	instantiation	171, 185, 172, 173, 174, 82, 83, 84	,  ⊢
	: , : , : , :
62	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
63	instantiation	250, 233, 238	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
65	instantiation	87, 252, 247, 211, 88, 212, 85, 193, 146	⊢
	: , : , : , : , : , :
66	instantiation	86, 211, 247, 212, 88, 193, 146	⊢
	: , : , : , :
67	instantiation	87, 252, 247, 211, 88, 212, 193, 146	⊢
	: , : , : , : , : , :
68	instantiation	93, 211, 247, 252, 212, 89, 193, 146, 90*	⊢
	: , : , : , : , : , :
69	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
70	instantiation	91	⊢
	:
71	instantiation	221	⊢
	: , :
72	instantiation	92, 252, 211, 212, 95, 146, 96	⊢
	: , : , : , : , : , : , :
73	instantiation	93, 211, 247, 252, 212, 94, 95, 96, 146, 97*	⊢
	: , : , : , : , : , :
74	instantiation	138, 98, 99	,  ⊢
	: , : , :
75	instantiation	197, 100, 101	,  ⊢
	: , : , :
76	instantiation	102, 123	⊢
	: , : , : , : , : , : , :
77	generalization	103	⊢
78	theorem		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
79	instantiation	104, 123, 156, 120	⊢
	: , : , : , : , : , : , : , :
80	modus ponens	105, 106	⊢
81	modus ponens	107, 108	⊢
82	instantiation	221	⊢
	: , :
83	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
84	instantiation	155, 174, 159, 177	,  ⊢
	: , : , : , :
85	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
86	theorem		⊢
	proveit.numbers.addition.elim_zero_any
87	theorem		⊢
	proveit.numbers.addition.disassociation
88	instantiation	221	⊢
	: , :
89	instantiation	221	⊢
	: , :
90	instantiation	151, 109, 165*	⊢
	: , :
91	axiom		⊢
	proveit.logic.equality.equals_reflexivity
92	theorem		⊢
	proveit.numbers.addition.leftward_commutation
93	theorem		⊢
	proveit.numbers.addition.association
94	instantiation	221	⊢
	: , :
95	instantiation	250, 225, 110	⊢
	: , : , :
96	instantiation	250, 225, 111	⊢
	: , : , :
97	instantiation	197, 112, 113, 114*	⊢
	: , : , :
98	instantiation	147, 115	,  ⊢
	: , : , :
99	instantiation	116, 195, 180, 137	,  ⊢
	: , : , :
100	instantiation	151, 117	,  ⊢
	: , :
101	instantiation	118, 249, 235	,  ⊢
	: , :
102	theorem		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
103	instantiation	119, 159, 120	,  ⊢
	: , :
104	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum_with_scalar_mult
105	instantiation	121, 123, 156	⊢
	: , : , : , : , : , :
106	generalization	139	⊢
107	instantiation	122, 252, 123, 211, 156, 212	⊢
	: , : , : , : , : , : , : , : , : , : , :
108	generalization	124	⊢
109	instantiation	144, 211, 247, 252, 212, 125, 164, 193, 131*	⊢
	: , : , : , : , : , :
110	instantiation	250, 228, 126	⊢
	: , : , :
111	instantiation	250, 228, 127	⊢
	: , : , :
112	instantiation	147, 128	⊢
	: , : , :
113	instantiation	151, 129	⊢
	: , :
114	instantiation	197, 130, 131	⊢
	: , : , :
115	instantiation	144, 132, 247, 211, 133, 134, 212, 215, 216, 219, 220, 214, 193	,  ⊢
	: , : , : , : , : , :
116	theorem		⊢
	proveit.numbers.exponentiation.product_of_complex_powers
117	instantiation	135, 136	,  ⊢
	: , : , :
118	theorem		⊢
	proveit.physics.quantum.algebra.prepend_num_ket_with_one_ket
119	theorem		⊢
	proveit.numbers.multiplication.commutation
120	instantiation	178, 179, 137	⊢
	: , :
121	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
122	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation_with_scalar_mult
123	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
124	instantiation	138, 139, 140	,  ⊢
	: , : , :
125	instantiation	221	⊢
	: , :
126	instantiation	250, 233, 141	⊢
	: , : , :
127	instantiation	250, 233, 142	⊢
	: , : , :
128	instantiation	151, 143	⊢
	: , :
129	instantiation	144, 211, 247, 252, 212, 145, 215, 146, 193	⊢
	: , : , : , : , : , :
130	instantiation	147, 148	⊢
	: , : , :
131	instantiation	149, 193	⊢
	:
132	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
133	instantiation	150	⊢
	: , : , : , :
134	instantiation	221	⊢
	: , :
135	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_eq
136	instantiation	151, 152	,  ⊢
	: , :
137	instantiation	201, 153, 154	⊢
	: , : , :
138	theorem		⊢
	proveit.logic.equality.sub_left_side_into
139	instantiation	155, 156, 159, 157	,  ⊢
	: , : , : , :
140	instantiation	158, 159, 252, 211, 212, 173, 174, 176, 177	,  ⊢
	: , : , : , : , : , : , : , : , : , :
141	instantiation	160, 243, 240	⊢
	: , :
142	instantiation	245, 240	⊢
	:
143	instantiation	161, 193	⊢
	:
144	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
145	instantiation	221	⊢
	: , :
146	instantiation	162, 164	⊢
	:
147	axiom		⊢
	proveit.logic.equality.substitution
148	instantiation	163, 164, 215, 165	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
150	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
151	theorem		⊢
	proveit.logic.equality.equals_reversal
152	instantiation	166, 214, 193	,  ⊢
	: , :
153	instantiation	218, 204, 167	⊢
	: , :
154	instantiation	197, 168, 169	⊢
	: , : , :
155	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
156	instantiation	170, 185, 172, 173, 174	⊢
	: , : , :
157	instantiation	171, 185, 172, 173, 174, 175, 176, 177	,  ⊢
	: , : , : , :
158	theorem		⊢
	proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod
159	instantiation	178, 179, 180	,  ⊢
	: , :
160	theorem		⊢
	proveit.numbers.multiplication.mult_int_closure_bin
161	theorem		⊢
	proveit.numbers.negation.mult_neg_one_left
162	theorem		⊢
	proveit.numbers.negation.complex_closure
163	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
164	instantiation	250, 225, 181	⊢
	: , : , :
165	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
166	theorem		⊢
	proveit.numbers.addition.commutation
167	instantiation	201, 182, 183	⊢
	: , : , :
168	instantiation	210, 252, 205, 211, 184, 212, 204, 219, 220, 193	⊢
	: , : , : , : , : , :
169	instantiation	210, 211, 247, 205, 212, 206, 184, 215, 216, 219, 220, 193	⊢
	: , : , : , : , : , :
170	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
171	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
172	instantiation	221	⊢
	: , :
173	instantiation	186, 185	⊢
	:
174	instantiation	186, 187	⊢
	:
175	instantiation	221	⊢
	: , :
176	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
177	instantiation	188, 249, 235	,  ⊢
	: , :
178	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
179	instantiation	250, 225, 189	⊢
	: , : , :
180	instantiation	201, 190, 191	,  ⊢
	: , : , :
181	instantiation	250, 228, 192	⊢
	: , : , :
182	instantiation	218, 209, 193	⊢
	: , :
183	instantiation	210, 211, 247, 252, 212, 213, 219, 220, 193	⊢
	: , : , : , : , : , :
184	instantiation	217	⊢
	: , : , :
185	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
186	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
187	instantiation	194, 247, 244	⊢
	: , :
188	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_in_register_space
189	instantiation	250, 230, 195	⊢
	: , : , :
190	instantiation	218, 204, 196	,  ⊢
	: , :
191	instantiation	197, 198, 199	,  ⊢
	: , : , :
192	instantiation	250, 233, 246	⊢
	: , : , :
193	instantiation	250, 225, 200	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
195	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
196	instantiation	201, 202, 203	,  ⊢
	: , : , :
197	axiom		⊢
	proveit.logic.equality.equals_transitivity
198	instantiation	210, 252, 205, 211, 207, 212, 204, 219, 220, 214	,  ⊢
	: , : , : , : , : , :
199	instantiation	210, 211, 247, 205, 212, 206, 207, 215, 216, 219, 220, 214	,  ⊢
	: , : , : , : , : , :
200	instantiation	250, 228, 208	⊢
	: , : , :
201	theorem		⊢
	proveit.logic.equality.sub_right_side_into
202	instantiation	218, 209, 214	,  ⊢
	: , :
203	instantiation	210, 211, 247, 252, 212, 213, 219, 220, 214	,  ⊢
	: , : , : , : , : , :
204	instantiation	218, 215, 216	⊢
	: , :
205	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
206	instantiation	221	⊢
	: , :
207	instantiation	217	⊢
	: , : , :
208	instantiation	250, 233, 240	⊢
	: , : , :
209	instantiation	218, 219, 220	⊢
	: , :
210	theorem		⊢
	proveit.numbers.multiplication.disassociation
211	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
212	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
213	instantiation	221	⊢
	: , :
214	instantiation	250, 225, 222	,  ⊢
	: , : , :
215	instantiation	250, 225, 223	⊢
	: , : , :
216	instantiation	250, 225, 224	⊢
	: , : , :
217	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
218	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
219	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
220	instantiation	250, 225, 226	⊢
	: , : , :
221	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
222	instantiation	250, 228, 227	,  ⊢
	: , : , :
223	instantiation	250, 228, 229	⊢
	: , : , :
224	instantiation	250, 230, 231	⊢
	: , : , :
225	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
226	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
227	instantiation	250, 233, 232	,  ⊢
	: , : , :
228	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
229	instantiation	250, 233, 243	⊢
	: , : , :
230	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
231	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
232	instantiation	250, 234, 235	,  ⊢
	: , : , :
233	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
234	instantiation	236, 237, 238	⊢
	: , :
235	assumption		⊢
236	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
237	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
238	instantiation	239, 240, 241	⊢
	: , :
239	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
240	instantiation	242, 243, 244	⊢
	: , :
241	instantiation	245, 246	⊢
	:
242	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
243	instantiation	250, 251, 247	⊢
	: , : , :
244	instantiation	250, 248, 249	⊢
	: , : , :
245	theorem		⊢
	proveit.numbers.negation.int_closure
246	instantiation	250, 251, 252	⊢
	: , : , :
247	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
248	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
249	assumption		⊢
250	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
251	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
252	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements