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	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
2	reference	231	⊢
3	instantiation	176	⊢
	: , :
4	instantiation	176	⊢
	: , :
5	instantiation	21, 7	⊢
	: , :
6	instantiation	180, 8	⊢
	: , : , :
7	instantiation	101, 9, 10, 11	⊢
	: , : , : , :
8	modus ponens	12, 13	⊢
9	instantiation	70, 142, 81, 82, 14*	⊢
	: , :
10	instantiation	180, 15	⊢
	: , : , :
11	instantiation	21, 16	⊢
	: , :
12	instantiation	17, 214	⊢
	: , : , : , : , : , :
13	generalization	18	⊢
14	instantiation	162, 19, 20	⊢
	: , : , :
15	instantiation	21, 22	⊢
	: , :
16	instantiation	162, 23, 24	⊢
	: , : , :
17	axiom		⊢
	proveit.core_expr_types.lambda_maps.lambda_substitution
18	instantiation	25, 26	⊢
	: , : , :
19	instantiation	180, 27	⊢
	: , : , :
20	instantiation	196, 28	⊢
	:
21	theorem		⊢
	proveit.logic.equality.equals_reversal
22	instantiation	29, 111, 197, 30*	⊢
	: , :
23	instantiation	180, 31	⊢
	: , : , :
24	instantiation	87, 197, 32, 206, 88	⊢
	: , : , :
25	axiom		⊢
	proveit.core_expr_types.conditionals.conditional_substitution
26	deduction	33	⊢
27	instantiation	87, 197, 171, 146, 88, 34*	⊢
	: , : , :
28	instantiation	90, 197, 35	⊢
	: , :
29	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
30	instantiation	101, 36, 37, 44	⊢
	: , : , : , :
31	instantiation	162, 38, 39	⊢
	: , : , :
32	instantiation	40, 130	⊢
	:
33	instantiation	106, 41, 42	,  ⊢
	: , :
34	instantiation	43, 150, 142, 44*	⊢
	: , :
35	instantiation	110, 150	⊢
	:
36	instantiation	154, 155, 231, 236, 156, 148, 149, 150, 197	⊢
	: , : , : , : , : , :
37	instantiation	162, 45, 46	⊢
	: , : , :
38	instantiation	180, 47	⊢
	: , : , :
39	instantiation	70, 142, 48, 49, 50*	⊢
	: , :
40	theorem		⊢
	proveit.numbers.negation.real_closure
41	instantiation	90, 52, 51	⊢
	: , :
42	instantiation	90, 52, 53	,  ⊢
	: , :
43	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
44	instantiation	183, 150	⊢
	:
45	instantiation	54, 155, 231, 156, 55, 149, 150, 197	⊢
	: , : , : , : , : , : , :
46	instantiation	162, 56, 57	⊢
	: , : , :
47	instantiation	180, 58	⊢
	: , : , :
48	instantiation	90, 197, 111	⊢
	: , :
49	instantiation	59, 168, 60	⊢
	: , :
50	instantiation	162, 61, 62	⊢
	: , : , :
51	instantiation	132, 63, 64	⊢
	: , : , :
52	instantiation	234, 205, 65	⊢
	: , : , :
53	instantiation	110, 66	,  ⊢
	:
54	theorem		⊢
	proveit.numbers.multiplication.rightward_commutation
55	instantiation	176	⊢
	: , :
56	instantiation	67, 236, 231, 155, 68, 156, 150, 197, 149	⊢
	: , : , : , : , : , :
57	instantiation	180, 69	⊢
	: , : , :
58	instantiation	70, 150, 197, 88, 71*	⊢
	: , :
59	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
60	instantiation	234, 72, 172	⊢
	: , : , :
61	instantiation	180, 73	⊢
	: , : , :
62	instantiation	196, 74	⊢
	:
63	instantiation	173, 135, 75	⊢
	: , :
64	instantiation	162, 76, 77	⊢
	: , : , :
65	instantiation	234, 194, 78	⊢
	: , : , :
66	instantiation	79, 80, 81, 82	,  ⊢
	: , :
67	theorem		⊢
	proveit.numbers.multiplication.association
68	instantiation	176	⊢
	: , :
69	instantiation	132, 83, 84	⊢
	: , : , :
70	theorem		⊢
	proveit.numbers.division.div_as_mult
71	instantiation	162, 85, 86	⊢
	: , : , :
72	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
73	instantiation	87, 197, 130, 146, 88, 89*	⊢
	: , : , :
74	instantiation	90, 197, 91	⊢
	: , :
75	instantiation	132, 92, 93	⊢
	: , : , :
76	instantiation	154, 236, 136, 155, 94, 156, 135, 174, 131, 175	⊢
	: , : , : , : , : , :
77	instantiation	154, 155, 231, 136, 156, 137, 94, 197, 159, 174, 131, 175	⊢
	: , : , : , : , : , :
78	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
79	theorem		⊢
	proveit.numbers.division.div_complex_closure
80	instantiation	132, 95, 96	,  ⊢
	: , : , :
81	instantiation	234, 205, 97	⊢
	: , : , :
82	instantiation	107, 98	⊢
	:
83	instantiation	132, 99, 100	⊢
	: , : , :
84	instantiation	101, 102, 103, 104	⊢
	: , : , : , :
85	instantiation	180, 105	⊢
	: , : , :
86	instantiation	106, 150, 149	⊢
	: , :
87	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
88	instantiation	107, 216	⊢
	:
89	instantiation	162, 108, 109	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
91	instantiation	110, 111	⊢
	:
92	instantiation	173, 112, 175	⊢
	: , :
93	instantiation	154, 155, 231, 236, 156, 113, 174, 131, 175	⊢
	: , : , : , : , : , :
94	instantiation	160	⊢
	: , : , :
95	instantiation	173, 135, 114	,  ⊢
	: , :
96	instantiation	162, 115, 116	,  ⊢
	: , : , :
97	instantiation	234, 212, 117	⊢
	: , : , :
98	instantiation	118, 231, 228	⊢
	: , :
99	instantiation	119, 142, 125, 120	⊢
	: , : , : , : , :
100	instantiation	162, 121, 122	⊢
	: , : , :
101	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
102	instantiation	180, 123	⊢
	: , : , :
103	instantiation	180, 123	⊢
	: , : , :
104	instantiation	183, 142	⊢
	:
105	instantiation	124, 125, 214, 126*	⊢
	: , :
106	theorem		⊢
	proveit.numbers.multiplication.commutation
107	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
108	instantiation	154, 155, 231, 236, 156, 148, 149, 150, 127	⊢
	: , : , : , : , : , :
109	instantiation	128, 231, 155, 148, 156, 149, 150, 142, 129*	⊢
	: , : , : , : , :
110	theorem		⊢
	proveit.numbers.negation.complex_closure
111	instantiation	234, 205, 130	⊢
	: , : , :
112	instantiation	173, 174, 131	⊢
	: , :
113	instantiation	176	⊢
	: , :
114	instantiation	132, 133, 134	,  ⊢
	: , : , :
115	instantiation	154, 236, 136, 155, 138, 156, 135, 174, 175, 158	,  ⊢
	: , : , : , : , : , :
116	instantiation	154, 155, 231, 136, 156, 137, 138, 197, 159, 174, 175, 158	,  ⊢
	: , : , : , : , : , :
117	instantiation	234, 219, 224	⊢
	: , : , :
118	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
119	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
120	instantiation	234, 143, 139	⊢
	: , : , :
121	instantiation	180, 140	⊢
	: , : , :
122	instantiation	180, 141	⊢
	: , : , :
123	instantiation	182, 142	⊢
	:
124	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
125	instantiation	234, 143, 144	⊢
	: , : , :
126	instantiation	145, 197	⊢
	:
127	instantiation	234, 205, 146	⊢
	: , : , :
128	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
129	instantiation	147, 231, 155, 148, 156, 149, 150	⊢
	: , : , : , :
130	instantiation	234, 212, 151	⊢
	: , : , :
131	instantiation	234, 205, 152	⊢
	: , : , :
132	theorem		⊢
	proveit.logic.equality.sub_right_side_into
133	instantiation	173, 153, 158	,  ⊢
	: , :
134	instantiation	154, 155, 231, 236, 156, 157, 174, 175, 158	,  ⊢
	: , : , : , : , : , :
135	instantiation	173, 197, 159	⊢
	: , :
136	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
137	instantiation	176	⊢
	: , :
138	instantiation	160	⊢
	: , : , :
139	instantiation	234, 167, 161	⊢
	: , : , :
140	instantiation	162, 163, 164	⊢
	: , : , :
141	instantiation	180, 165	⊢
	: , : , :
142	instantiation	234, 205, 166	⊢
	: , : , :
143	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
144	instantiation	234, 167, 168	⊢
	: , : , :
145	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
146	instantiation	234, 212, 169	⊢
	: , : , :
147	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
148	instantiation	176	⊢
	: , :
149	instantiation	234, 205, 170	⊢
	: , : , :
150	instantiation	234, 205, 171	⊢
	: , : , :
151	instantiation	234, 199, 172	⊢
	: , : , :
152	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
153	instantiation	173, 174, 175	⊢
	: , :
154	theorem		⊢
	proveit.numbers.multiplication.disassociation
155	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
156	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
157	instantiation	176	⊢
	: , :
158	instantiation	234, 205, 177	⊢
	: , : , :
159	instantiation	234, 205, 178	⊢
	: , : , :
160	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
161	instantiation	234, 185, 179	⊢
	: , : , :
162	axiom		⊢
	proveit.logic.equality.equals_transitivity
163	instantiation	180, 181	⊢
	: , : , :
164	instantiation	182, 197	⊢
	:
165	instantiation	183, 197	⊢
	:
166	instantiation	234, 212, 184	⊢
	: , : , :
167	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
168	instantiation	234, 185, 186	⊢
	: , : , :
169	instantiation	234, 219, 225	⊢
	: , : , :
170	instantiation	234, 212, 187	⊢
	: , : , :
171	instantiation	188, 189, 233	⊢
	: , : , :
172	instantiation	190, 200, 191	⊢
	: , :
173	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
174	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
175	instantiation	234, 205, 192	⊢
	: , : , :
176	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
177	instantiation	234, 212, 193	⊢
	: , : , :
178	instantiation	234, 194, 195	⊢
	: , : , :
179	instantiation	234, 198, 214	⊢
	: , : , :
180	axiom		⊢
	proveit.logic.equality.substitution
181	instantiation	196, 197	⊢
	:
182	theorem		⊢
	proveit.numbers.division.frac_one_denom
183	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
184	instantiation	234, 219, 230	⊢
	: , : , :
185	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
186	instantiation	234, 198, 216	⊢
	: , : , :
187	instantiation	234, 199, 200	⊢
	: , : , :
188	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
189	instantiation	201, 202	⊢
	: , :
190	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
191	instantiation	234, 215, 233	⊢
	: , : , :
192	instantiation	234, 212, 203	⊢
	: , : , :
193	instantiation	234, 219, 204	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
195	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
196	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
197	instantiation	234, 205, 206	⊢
	: , : , :
198	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
199	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
200	instantiation	207, 208, 209	⊢
	: , :
201	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
202	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
203	instantiation	234, 219, 210	⊢
	: , : , :
204	instantiation	234, 217, 211	⊢
	: , : , :
205	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
206	instantiation	234, 212, 213	⊢
	: , : , :
207	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
208	instantiation	234, 215, 214	⊢
	: , : , :
209	instantiation	234, 215, 216	⊢
	: , : , :
210	instantiation	234, 217, 218	⊢
	: , : , :
211	assumption		⊢
212	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
213	instantiation	234, 219, 227	⊢
	: , : , :
214	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
215	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
216	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
217	instantiation	220, 221, 222	⊢
	: , :
218	assumption		⊢
219	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
220	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
221	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
222	instantiation	223, 224, 225	⊢
	: , :
223	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
224	instantiation	226, 227, 228	⊢
	: , :
225	instantiation	229, 230	⊢
	:
226	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
227	instantiation	234, 235, 231	⊢
	: , : , :
228	instantiation	234, 232, 233	⊢
	: , : , :
229	theorem		⊢
	proveit.numbers.negation.int_closure
230	instantiation	234, 235, 236	⊢
	: , : , :
231	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
232	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
233	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
234	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
235	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
236	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements