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, 4, 5, 6*	⊢
	: , : , : , : , :
1	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled
2	instantiation	7, 199, 9, 25, 38	⊢
	: , : , :
3	instantiation	8, 199, 9, 25, 38, 10, 11, 12	⊢
	: , : , : , :
4	reference	14	⊢
5	reference	15	⊢
6	instantiation	13, 14, 15	⊢
	: , :
7	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
8	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
9	instantiation	145	⊢
	: , :
10	instantiation	145	⊢
	: , :
11	instantiation	16, 25, 17, 18	⊢
	: , : , : , :
12	modus ponens	19, 20	⊢
13	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
14	instantiation	68, 144, 21, 22	⊢
	: , :
15	instantiation	68, 144, 23, 24	⊢
	: , :
16	theorem		⊢
	proveit.linear_algebra.addition.binary_closure
17	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
18	instantiation	37, 25, 26, 27	⊢
	: , : , : , :
19	instantiation	28, 197, 38	⊢
	: , : , : , : , : , :
20	generalization	29	⊢
21	instantiation	51, 161, 30	⊢
	: , :
22	instantiation	33, 31, 32	⊢
	: , : , :
23	instantiation	51, 161, 55	⊢
	: , :
24	instantiation	33, 34, 35	⊢
	: , : , :
25	instantiation	49, 199	⊢
	:
26	instantiation	51, 52, 36	⊢
	: , :
27	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
28	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
29	instantiation	37, 38, 39, 40	,  ⊢
	: , : , : , :
30	instantiation	142, 41, 42	⊢
	: , :
31	instantiation	45, 170, 43	⊢
	: , :
32	instantiation	137, 44	⊢
	: , : , :
33	theorem		⊢
	proveit.logic.equality.sub_left_side_into
34	instantiation	45, 170, 46	⊢
	: , :
35	instantiation	137, 97	⊢
	: , : , :
36	instantiation	89, 47, 48	⊢
	: , : , :
37	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
38	instantiation	49, 50	⊢
	:
39	instantiation	51, 52, 53	,  ⊢
	: , :
40	instantiation	54, 195, 154	,  ⊢
	: , :
41	instantiation	68, 131, 161, 111	⊢
	: , :
42	instantiation	98, 55	⊢
	:
43	instantiation	56, 57, 170	⊢
	: , :
44	instantiation	123, 58, 59	⊢
	: , : , :
45	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
46	instantiation	200, 60, 140	⊢
	: , : , :
47	instantiation	115, 92, 61	⊢
	: , :
48	instantiation	123, 62, 63	⊢
	: , : , :
49	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
50	instantiation	64, 202, 185	⊢
	: , :
51	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
52	instantiation	200, 171, 65	⊢
	: , : , :
53	instantiation	89, 66, 67	,  ⊢
	: , : , :
54	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_in_register_space
55	instantiation	68, 143, 161, 111	⊢
	: , :
56	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
57	instantiation	200, 180, 69	⊢
	: , : , :
58	instantiation	123, 70, 71	⊢
	: , : , :
59	instantiation	123, 72, 73	⊢
	: , : , :
60	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
61	instantiation	89, 74, 75	⊢
	: , : , :
62	instantiation	103, 196, 93, 133, 76, 135, 92, 116, 117, 88	⊢
	: , : , : , : , : , :
63	instantiation	103, 133, 202, 93, 135, 94, 76, 161, 106, 116, 117, 88	⊢
	: , : , : , : , : , :
64	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
65	instantiation	200, 129, 77	⊢
	: , : , :
66	instantiation	115, 92, 78	,  ⊢
	: , :
67	instantiation	123, 79, 80	,  ⊢
	: , : , :
68	theorem		⊢
	proveit.numbers.division.div_complex_closure
69	instantiation	200, 191, 197	⊢
	: , : , :
70	instantiation	137, 81	⊢
	: , : , :
71	instantiation	137, 82	⊢
	: , : , :
72	instantiation	83, 133, 202, 196, 135, 84, 99, 147, 85	⊢
	: , : , : , : , : , :
73	instantiation	86, 99, 147, 87	⊢
	: , : , :
74	instantiation	115, 102, 88	⊢
	: , :
75	instantiation	103, 133, 202, 196, 135, 104, 116, 117, 88	⊢
	: , : , : , : , : , :
76	instantiation	107	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
78	instantiation	89, 90, 91	,  ⊢
	: , : , :
79	instantiation	103, 196, 93, 133, 95, 135, 92, 116, 117, 105	,  ⊢
	: , : , : , : , : , :
80	instantiation	103, 133, 202, 93, 135, 94, 95, 161, 106, 116, 117, 105	,  ⊢
	: , : , : , : , : , :
81	instantiation	110, 131, 161, 111, 96*	⊢
	: , :
82	instantiation	137, 97	⊢
	: , : , :
83	theorem		⊢
	proveit.numbers.addition.disassociation
84	instantiation	145	⊢
	: , :
85	instantiation	98, 99	⊢
	:
86	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
87	instantiation	100	⊢
	:
88	instantiation	200, 171, 101	⊢
	: , : , :
89	theorem		⊢
	proveit.logic.equality.sub_right_side_into
90	instantiation	115, 102, 105	,  ⊢
	: , :
91	instantiation	103, 133, 202, 196, 135, 104, 116, 117, 105	,  ⊢
	: , : , : , : , : , :
92	instantiation	115, 161, 106	⊢
	: , :
93	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
94	instantiation	145	⊢
	: , :
95	instantiation	107	⊢
	: , : , :
96	instantiation	123, 108, 109	⊢
	: , : , :
97	instantiation	110, 143, 161, 111, 112*	⊢
	: , :
98	theorem		⊢
	proveit.numbers.negation.complex_closure
99	instantiation	200, 171, 113	⊢
	: , : , :
100	axiom		⊢
	proveit.logic.equality.equals_reflexivity
101	instantiation	200, 182, 114	⊢
	: , : , :
102	instantiation	115, 116, 117	⊢
	: , :
103	theorem		⊢
	proveit.numbers.multiplication.disassociation
104	instantiation	145	⊢
	: , :
105	instantiation	200, 171, 118	,  ⊢
	: , : , :
106	instantiation	200, 171, 119	⊢
	: , : , :
107	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
108	instantiation	137, 138	⊢
	: , : , :
109	instantiation	123, 120, 121	⊢
	: , : , :
110	theorem		⊢
	proveit.numbers.division.div_as_mult
111	instantiation	122, 199	⊢
	:
112	instantiation	123, 124, 125	⊢
	: , : , :
113	instantiation	200, 182, 126	⊢
	: , : , :
114	instantiation	200, 192, 174	⊢
	: , : , :
115	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
116	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
117	instantiation	200, 171, 127	⊢
	: , : , :
118	instantiation	200, 182, 128	,  ⊢
	: , : , :
119	instantiation	200, 129, 130	⊢
	: , : , :
120	instantiation	139, 131, 147	⊢
	: , :
121	instantiation	132, 196, 202, 133, 134, 135, 147, 143, 144, 136*	⊢
	: , : , : , : , : , :
122	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
123	axiom		⊢
	proveit.logic.equality.equals_transitivity
124	instantiation	137, 138	⊢
	: , : , :
125	instantiation	139, 143, 147	⊢
	: , :
126	instantiation	200, 178, 140	⊢
	: , : , :
127	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
128	instantiation	200, 192, 141	,  ⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
130	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
131	instantiation	142, 143, 144	⊢
	: , :
132	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
133	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
134	instantiation	145	⊢
	: , :
135	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
136	instantiation	146, 147	⊢
	:
137	axiom		⊢
	proveit.logic.equality.substitution
138	instantiation	148, 149, 197, 150*	⊢
	: , :
139	theorem		⊢
	proveit.numbers.multiplication.commutation
140	instantiation	151, 179, 152	⊢
	: , :
141	instantiation	200, 153, 154	,  ⊢
	: , : , :
142	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
143	instantiation	200, 171, 155	⊢
	: , : , :
144	instantiation	200, 171, 156	⊢
	: , : , :
145	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
146	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
147	instantiation	200, 171, 157	⊢
	: , : , :
148	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
149	instantiation	200, 158, 159	⊢
	: , : , :
150	instantiation	160, 161	⊢
	:
151	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
152	instantiation	200, 198, 195	⊢
	: , : , :
153	instantiation	162, 163, 164	⊢
	: , :
154	assumption		⊢
155	instantiation	165, 166, 195	⊢
	: , : , :
156	instantiation	200, 182, 167	⊢
	: , : , :
157	instantiation	200, 182, 168	⊢
	: , : , :
158	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
159	instantiation	200, 169, 170	⊢
	: , : , :
160	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
161	instantiation	200, 171, 172	⊢
	: , : , :
162	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
163	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
164	instantiation	173, 174, 175	⊢
	: , :
165	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
166	instantiation	176, 177	⊢
	: , :
167	instantiation	200, 192, 187	⊢
	: , : , :
168	instantiation	200, 178, 179	⊢
	: , : , :
169	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
170	instantiation	200, 180, 181	⊢
	: , : , :
171	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
172	instantiation	200, 182, 183	⊢
	: , : , :
173	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
174	instantiation	184, 193, 185	⊢
	: , :
175	instantiation	186, 187	⊢
	:
176	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
177	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
178	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
179	instantiation	188, 189, 190	⊢
	: , :
180	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
181	instantiation	200, 191, 199	⊢
	: , : , :
182	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
183	instantiation	200, 192, 193	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
185	instantiation	200, 194, 195	⊢
	: , : , :
186	theorem		⊢
	proveit.numbers.negation.int_closure
187	instantiation	200, 201, 196	⊢
	: , : , :
188	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
189	instantiation	200, 198, 197	⊢
	: , : , :
190	instantiation	200, 198, 199	⊢
	: , : , :
191	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
192	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
193	instantiation	200, 201, 202	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
195	assumption		⊢
196	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
197	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
198	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
199	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
200	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
201	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
202	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements