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