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	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
2	instantiation	189, 4, 13	⊢
	: , : , :
3	instantiation	5, 327, 19, 6, 21, 22, 7, 8*	⊢
	: , : , : , :
4	instantiation	243, 9, 10	⊢
	: , : , :
5	theorem		⊢
	proveit.linear_algebra.tensors.norm_preserving_tensor_prod
6	instantiation	30, 316, 317, 133, 45	⊢
	: , : , :
7	modus ponens	11, 12	⊢
8	instantiation	210, 13	⊢
	: , :
9	instantiation	14, 327, 15, 16, 17*	⊢
	: , : , :
10	instantiation	18, 327, 19, 20, 21, 22	⊢
	: , : , : , :
11	instantiation	44, 316, 317, 45	⊢
	: , : , : , :
12	generalization	23	⊢
13	instantiation	24, 327	⊢
	:
14	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
15	instantiation	106, 25, 203, 32	⊢
	: , : , : , :
16	instantiation	30, 316, 317, 259, 45	⊢
	: , : , :
17	instantiation	26, 27, 296, 42, 28*, 42*	⊢
	: , :
18	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
19	instantiation	106, 29, 203, 32	⊢
	: , : , : , :
20	instantiation	30, 316, 317, 129, 45	⊢
	: , : , :
21	instantiation	106, 31, 203, 32	⊢
	: , : , : , :
22	modus ponens	33, 34	⊢
23	instantiation	252, 35, 36	,  ⊢
	: , : , :
24	axiom		⊢
	proveit.physics.quantum.QPE._psi_t_def
25	instantiation	260, 37, 42	⊢
	: , : , :
26	theorem		⊢
	proveit.numbers.exponentiation.exp_nat_pos_rev
27	instantiation	148, 310, 277, 38, 278, 82, 324, 149	⊢
	: , : , : , : , :
28	instantiation	210, 39	⊢
	: , :
29	instantiation	260, 40, 42	⊢
	: , : , :
30	theorem		⊢
	proveit.logic.booleans.conjunction.redundant_conjunction_general
31	instantiation	260, 41, 42	⊢
	: , : , :
32	instantiation	210, 43	⊢
	: , :
33	instantiation	44, 316, 317, 45	⊢
	: , : , : , :
34	generalization	46	⊢
35	instantiation	101, 133, 66, 67, 47*, 48*	,  ⊢
	: , : , : , :
36	instantiation	252, 49, 50	⊢
	: , : , :
37	instantiation	55, 56	⊢
	: , : , :
38	instantiation	289	⊢
	: , :
39	instantiation	51, 319, 52, 53, 54	⊢
	: , : , : , : , : , :
40	instantiation	55, 56	⊢
	: , : , :
41	instantiation	55, 56	⊢
	: , : , :
42	instantiation	252, 57, 58	⊢
	: , : , :
43	instantiation	59, 60	⊢
	: , :
44	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
45	instantiation	177, 61, 62, 222, 63, 64*, 65*	⊢
	: , : , :
46	instantiation	128, 129, 66, 67	,  ⊢
	: , : , : , :
47	instantiation	68, 69	⊢
	:
48	instantiation	70, 129, 134, 96, 71, 72*	,  ⊢
	: , : , : , :
49	instantiation	234, 73	⊢
	: , : , :
50	instantiation	260, 74, 75	⊢
	: , : , :
51	theorem		⊢
	proveit.core_expr_types.tuples.shift_equivalence
52	instantiation	76, 77, 82	⊢
	: , :
53	instantiation	210, 78	⊢
	: , :
54	instantiation	210, 79	⊢
	: , :
55	theorem		⊢
	proveit.core_expr_types.tuples.range_len
56	instantiation	80, 264, 81, 277, 82, 324	⊢
	: , :
57	instantiation	234, 83	⊢
	: , : , :
58	instantiation	106, 84, 85, 86	⊢
	: , : , : , :
59	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
60	instantiation	325, 110, 327	⊢
	: , : , :
61	instantiation	325, 308, 87	⊢
	: , : , :
62	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
63	instantiation	88, 89	⊢
	: , :
64	instantiation	252, 90, 91	⊢
	: , : , :
65	instantiation	106, 92, 122, 93	⊢
	: , : , : , :
66	instantiation	325, 305, 94	⊢
	: , : , :
67	instantiation	95, 129, 134, 96	,  ⊢
	: , : , : , :
68	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
69	instantiation	97, 98	⊢
	:
70	theorem		⊢
	proveit.linear_algebra.addition.norm_of_sum_of_orthogonal_pair
71	instantiation	260, 99, 100	,  ⊢
	: , : , :
72	instantiation	101, 133, 185, 135, 102*	,  ⊢
	: , : , : , :
73	instantiation	234, 103	⊢
	: , : , :
74	instantiation	260, 104, 105	⊢
	: , : , :
75	instantiation	106, 107, 108, 109	⊢
	: , : , : , :
76	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
77	instantiation	325, 110, 111	⊢
	: , : , :
78	instantiation	252, 112, 113	⊢
	: , : , :
79	instantiation	252, 114, 115	⊢
	: , : , :
80	theorem		⊢
	proveit.numbers.addition.add_nat_closure
81	instantiation	282	⊢
	: , : , :
82	instantiation	283, 116	⊢
	:
83	instantiation	117, 200, 199, 152*	⊢
	: , :
84	instantiation	173, 324, 310, 118, 163, 202, 120, 199	⊢
	: , : , : , : , : , :
85	instantiation	124, 277, 264, 278, 119, 202, 120, 199	⊢
	: , : , : , :
86	instantiation	121, 199, 202, 122	⊢
	: , : , :
87	instantiation	325, 311, 316	⊢
	: , : , :
88	theorem		⊢
	proveit.numbers.ordering.relax_less
89	instantiation	123, 327	⊢
	:
90	instantiation	173, 324, 310, 277, 174, 278, 163, 200, 199	⊢
	: , : , : , : , : , :
91	instantiation	124, 277, 310, 278, 174, 200, 199	⊢
	: , : , : , :
92	instantiation	252, 125, 126	⊢
	: , : , :
93	instantiation	210, 127	⊢
	: , :
94	instantiation	325, 298, 131	⊢
	: , : , :
95	theorem		⊢
	proveit.linear_algebra.addition.binary_closure
96	instantiation	128, 129, 185, 135	,  ⊢
	: , : , : , :
97	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
98	instantiation	325, 130, 131	⊢
	: , : , :
99	instantiation	132, 133, 185, 134, 135	,  ⊢
	: , : , : , : , :
100	instantiation	252, 136, 137	,  ⊢
	: , : , :
101	theorem		⊢
	proveit.linear_algebra.inner_products.scaled_norm
102	instantiation	252, 138, 139	,  ⊢
	: , : , :
103	instantiation	252, 140, 141	⊢
	: , : , :
104	instantiation	142, 199, 143, 144	⊢
	: , : , : , : , :
105	instantiation	252, 145, 146	⊢
	: , : , :
106	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
107	instantiation	234, 147	⊢
	: , : , :
108	instantiation	234, 147	⊢
	: , : , :
109	instantiation	239, 199	⊢
	:
110	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
111	instantiation	148, 324, 277, 278, 149	⊢
	: , : , : , : , :
112	instantiation	234, 152	⊢
	: , : , :
113	instantiation	252, 150, 151	⊢
	: , : , :
114	instantiation	234, 152	⊢
	: , : , :
115	instantiation	155, 202	⊢
	:
116	instantiation	293, 316, 153	⊢
	:
117	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
118	instantiation	289	⊢
	: , :
119	instantiation	282	⊢
	: , : , :
120	instantiation	302, 199	⊢
	:
121	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
122	instantiation	223	⊢
	:
123	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
124	theorem		⊢
	proveit.numbers.addition.elim_zero_any
125	instantiation	173, 324, 310, 277, 174, 278, 202, 200, 199	⊢
	: , : , : , : , : , :
126	instantiation	154, 202, 199, 203	⊢
	: , : , :
127	instantiation	155, 199	⊢
	:
128	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
129	instantiation	156, 259	⊢
	:
130	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonneg
131	instantiation	157, 158, 205, 159	⊢
	: , :
132	theorem		⊢
	proveit.linear_algebra.inner_products.inner_prod_scalar_mult_right
133	instantiation	160, 259	⊢
	:
134	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
135	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
136	instantiation	234, 161	⊢
	: , : , :
137	instantiation	162, 185, 163, 164*	,  ⊢
	: , :
138	instantiation	234, 165	,  ⊢
	: , : , :
139	instantiation	217, 166	⊢
	:
140	instantiation	252, 167, 168	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
142	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
143	instantiation	325, 170, 169	⊢
	: , : , :
144	instantiation	325, 170, 183	⊢
	: , : , :
145	instantiation	234, 171	⊢
	: , : , :
146	instantiation	234, 172	⊢
	: , : , :
147	instantiation	219, 199	⊢
	:
148	theorem		⊢
	proveit.numbers.addition.add_nat_pos_from_nonneg
149	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
150	instantiation	173, 277, 310, 324, 278, 174, 200, 199, 202	⊢
	: , : , : , : , : , :
151	instantiation	175, 202, 199, 203	⊢
	: , : , :
152	instantiation	176, 202	⊢
	:
153	instantiation	177, 221, 220, 222, 178, 179*, 180*	⊢
	: , : , :
154	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
155	theorem		⊢
	proveit.numbers.addition.elim_zero_left
156	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
157	theorem		⊢
	proveit.numbers.division.div_real_pos_closure
158	instantiation	325, 245, 181	⊢
	: , : , :
159	instantiation	182, 183	⊢
	:
160	theorem		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_inner_prod_space
161	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_and_one_have_zero_inner_prod
162	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
163	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
164	instantiation	184, 185	,  ⊢
	:
165	instantiation	186, 187, 188*	,  ⊢
	:
166	instantiation	189, 199, 235	⊢
	: , : , :
167	instantiation	234, 190	⊢
	: , : , :
168	instantiation	234, 191	⊢
	: , : , :
169	instantiation	325, 192, 193	⊢
	: , : , :
170	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
171	instantiation	234, 194	⊢
	: , : , :
172	instantiation	252, 195, 196	⊢
	: , : , :
173	theorem		⊢
	proveit.numbers.addition.disassociation
174	instantiation	289	⊢
	: , :
175	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_31
176	theorem		⊢
	proveit.numbers.negation.double_negation
177	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
178	instantiation	197, 327	⊢
	:
179	instantiation	198, 199, 200	⊢
	: , :
180	instantiation	201, 202, 203	⊢
	: , :
181	instantiation	325, 258, 238	⊢
	: , : , :
182	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
183	instantiation	325, 204, 205	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
185	instantiation	295, 206, 207	,  ⊢
	: , :
186	theorem		⊢
	proveit.numbers.absolute_value.complex_unit_length
187	instantiation	260, 208, 209	,  ⊢
	: , : , :
188	instantiation	210, 211	,  ⊢
	: , :
189	theorem		⊢
	proveit.logic.equality.sub_left_side_into
190	instantiation	252, 212, 214	⊢
	: , : , :
191	instantiation	252, 213, 214	⊢
	: , : , :
192	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
193	instantiation	325, 215, 216	⊢
	: , : , :
194	instantiation	217, 240	⊢
	:
195	instantiation	234, 218	⊢
	: , : , :
196	instantiation	219, 240	⊢
	:
197	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
198	theorem		⊢
	proveit.numbers.addition.commutation
199	instantiation	325, 305, 220	⊢
	: , : , :
200	instantiation	325, 305, 221	⊢
	: , : , :
201	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
202	instantiation	325, 305, 222	⊢
	: , : , :
203	instantiation	223	⊢
	:
204	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
205	instantiation	224, 225	⊢
	:
206	instantiation	325, 305, 226	⊢
	: , : , :
207	instantiation	260, 227, 228	,  ⊢
	: , : , :
208	instantiation	291, 281, 229	,  ⊢
	: , :
209	instantiation	252, 230, 231	,  ⊢
	: , : , :
210	theorem		⊢
	proveit.logic.equality.equals_reversal
211	instantiation	234, 232	,  ⊢
	: , : , :
212	instantiation	234, 233	⊢
	: , : , :
213	instantiation	234, 235	⊢
	: , : , :
214	instantiation	236, 296	⊢
	:
215	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
216	instantiation	325, 237, 238	⊢
	: , : , :
217	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
218	instantiation	239, 240	⊢
	:
219	theorem		⊢
	proveit.numbers.division.frac_one_denom
220	instantiation	325, 308, 241	⊢
	: , : , :
221	instantiation	325, 308, 242	⊢
	: , : , :
222	instantiation	243, 244, 327	⊢
	: , : , :
223	axiom		⊢
	proveit.logic.equality.equals_reflexivity
224	theorem		⊢
	proveit.numbers.exponentiation.sqrt_real_pos_closure
225	instantiation	325, 245, 246	⊢
	: , : , :
226	instantiation	325, 298, 247	⊢
	: , : , :
227	instantiation	286, 263, 248	,  ⊢
	: , :
228	instantiation	252, 249, 250	,  ⊢
	: , : , :
229	instantiation	291, 251, 290	,  ⊢
	: , :
230	instantiation	276, 324, 310, 277, 270, 278, 263, 288, 280	,  ⊢
	: , : , : , : , : , :
231	instantiation	276, 277, 310, 278, 269, 270, 296, 274, 288, 280	,  ⊢
	: , : , : , : , : , :
232	instantiation	252, 253, 254	,  ⊢
	: , : , :
233	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_norm
234	axiom		⊢
	proveit.logic.equality.substitution
235	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_norm
236	theorem		⊢
	proveit.numbers.exponentiation.exponentiated_one
237	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
238	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
239	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
240	instantiation	255, 296	⊢
	:
241	instantiation	325, 311, 320	⊢
	: , : , :
242	instantiation	325, 311, 319	⊢
	: , : , :
243	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
244	instantiation	256, 257	⊢
	: , :
245	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
246	instantiation	325, 258, 259	⊢
	: , : , :
247	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
248	instantiation	260, 261, 262	,  ⊢
	: , : , :
249	instantiation	276, 324, 264, 277, 265, 278, 263, 287, 288, 280	,  ⊢
	: , : , : , : , : , :
250	instantiation	276, 277, 310, 264, 278, 269, 265, 296, 274, 287, 288, 280	,  ⊢
	: , : , : , : , : , :
251	instantiation	266, 301, 267	,  ⊢
	: , :
252	axiom		⊢
	proveit.logic.equality.equals_transitivity
253	instantiation	268, 277, 310, 278, 269, 270, 296, 274, 287, 288, 280	,  ⊢
	: , : , : , : , : , : , :
254	instantiation	271, 324, 272, 277, 273, 278, 287, 296, 274, 288, 280	,  ⊢
	: , : , : , : , : , :
255	theorem		⊢
	proveit.numbers.exponentiation.sqrt_complex_closure
256	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
257	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
258	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
259	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
260	theorem		⊢
	proveit.logic.equality.sub_right_side_into
261	instantiation	286, 275, 280	,  ⊢
	: , :
262	instantiation	276, 277, 310, 324, 278, 279, 287, 288, 280	,  ⊢
	: , : , : , : , : , :
263	instantiation	325, 305, 281	⊢
	: , : , :
264	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
265	instantiation	282	⊢
	: , : , :
266	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
267	instantiation	283, 284	,  ⊢
	:
268	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
269	instantiation	289	⊢
	: , :
270	instantiation	289	⊢
	: , :
271	theorem		⊢
	proveit.numbers.multiplication.association
272	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
273	instantiation	285	⊢
	: , : , : , :
274	instantiation	325, 305, 292	⊢
	: , : , :
275	instantiation	286, 287, 288	,  ⊢
	: , :
276	theorem		⊢
	proveit.numbers.multiplication.disassociation
277	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
278	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
279	instantiation	289	⊢
	: , :
280	instantiation	325, 305, 290	⊢
	: , : , :
281	instantiation	291, 301, 292	⊢
	: , :
282	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
283	theorem		⊢
	proveit.numbers.negation.nat_closure
284	instantiation	293, 312, 294	,  ⊢
	:
285	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
286	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
287	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
288	instantiation	295, 296, 297	,  ⊢
	: , :
289	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
290	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
291	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
292	instantiation	325, 298, 299	⊢
	: , : , :
293	theorem		⊢
	proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
294	instantiation	300, 316, 317, 314	,  ⊢
	: , : , :
295	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
296	instantiation	325, 305, 301	⊢
	: , : , :
297	instantiation	302, 303	,  ⊢
	:
298	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
299	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
300	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
301	instantiation	325, 308, 304	⊢
	: , : , :
302	theorem		⊢
	proveit.numbers.negation.complex_closure
303	instantiation	325, 305, 306	,  ⊢
	: , : , :
304	instantiation	325, 311, 307	⊢
	: , : , :
305	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
306	instantiation	325, 308, 309	,  ⊢
	: , : , :
307	instantiation	325, 323, 310	⊢
	: , : , :
308	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
309	instantiation	325, 311, 312	,  ⊢
	: , : , :
310	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
311	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
312	instantiation	325, 313, 314	,  ⊢
	: , : , :
313	instantiation	315, 316, 317	⊢
	: , :
314	assumption		⊢
315	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
316	instantiation	318, 319, 320	⊢
	: , :
317	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
318	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
319	instantiation	321, 322	⊢
	:
320	instantiation	325, 323, 324	⊢
	: , : , :
321	theorem		⊢
	proveit.numbers.negation.int_closure
322	instantiation	325, 326, 327	⊢
	: , : , :
323	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
324	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
325	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
326	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
327	assumption		⊢
*equality replacement requirements