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	reference	10	⊢
2	instantiation	30, 3, 4, 5	, , ,  ⊢
	: , : , : , :
3	instantiation	152, 6, 7	, , ,  ⊢
	: , : , :
4	instantiation	152, 8, 9	, , ,  ⊢
	: , : , :
5	instantiation	10, 11	, , ,  ⊢
	: , :
6	instantiation	37, 12	, , ,  ⊢
	: , : , :
7	instantiation	13, 14, 45, 15, 16*	, , ,  ⊢
	: , :
8	instantiation	87, 194, 189, 17, 95, 96, 45, 105, 98	, , ,  ⊢
	: , : , : , : , : , : , :
9	instantiation	87, 189, 194, 18, 95, 105, 96, 45, 98	, , ,  ⊢
	: , : , : , : , : , : , :
10	theorem		⊢
	proveit.logic.equality.equals_reversal
11	instantiation	152, 19, 20	, , ,  ⊢
	: , : , :
12	instantiation	152, 21, 22	, , ,  ⊢
	: , : , :
13	theorem		⊢
	proveit.numbers.division.div_as_mult
14	instantiation	56, 23, 24	, , ,  ⊢
	: , : , :
15	instantiation	25, 133, 128, 117	⊢
	: , :
16	instantiation	152, 26, 27	, , ,  ⊢
	: , : , :
17	instantiation	175	⊢
	: , :
18	instantiation	175	⊢
	: , :
19	instantiation	152, 28, 29	, , ,  ⊢
	: , : , :
20	instantiation	87, 88, 189, 90, 42, 44, 105, 45, 95, 96, 98	, , ,  ⊢
	: , : , : , : , : , : , :
21	instantiation	30, 31, 32, 33	, , ,  ⊢
	: , : , : , :
22	instantiation	87, 88, 189, 90, 53, 94, 96, 133, 95, 105, 98	, , ,  ⊢
	: , : , : , : , : , : , :
23	instantiation	104, 59, 34	, , ,  ⊢
	: , :
24	instantiation	152, 35, 36	, , ,  ⊢
	: , : , :
25	theorem		⊢
	proveit.numbers.exponentiation.exp_not_eq_zero
26	instantiation	37, 38	⊢
	: , : , :
27	instantiation	152, 39, 40	, , ,  ⊢
	: , : , :
28	instantiation	87, 172, 194, 41, 105, 45, 177, 96, 46, 98	, , ,  ⊢
	: , : , : , : , : , : , :
29	instantiation	91, 189, 42, 43, 44, 105, 45, 177, 46, 96, 98, 47*	, , ,  ⊢
	: , : , : , : , : , :
30	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
31	instantiation	152, 48, 49	, , ,  ⊢
	: , : , :
32	instantiation	91, 88, 189, 64, 90, 50, 51, 111, 133, 108, 73, 105, 98, 52*	, , ,  ⊢
	: , : , : , : , : , :
33	instantiation	91, 189, 53, 54, 94, 96, 133, 108, 73, 105, 98, 55*	, , ,  ⊢
	: , : , : , : , : , :
34	instantiation	56, 57, 58	, ,  ⊢
	: , : , :
35	instantiation	83, 194, 172, 88, 60, 90, 59, 133, 105, 98	, , ,  ⊢
	: , : , : , : , : , :
36	instantiation	83, 88, 189, 172, 90, 92, 60, 95, 96, 133, 105, 98	, , ,  ⊢
	: , : , : , : , : , :
37	axiom		⊢
	proveit.logic.equality.substitution
38	instantiation	61, 133, 146, 62, 117, 63*	⊢
	: , : , :
39	instantiation	83, 88, 64, 194, 90, 65, 95, 96, 133, 105, 98, 97	, , ,  ⊢
	: , : , : , : , : , :
40	instantiation	152, 66, 67	, , ,  ⊢
	: , : , :
41	instantiation	106	⊢
	: , : , :
42	instantiation	175	⊢
	: , :
43	instantiation	175	⊢
	: , :
44	instantiation	175	⊢
	: , :
45	instantiation	68, 133	⊢
	:
46	instantiation	107, 177, 109, 110	⊢
	: , :
47	instantiation	76, 177, 77, 78, 69*, 70*, 81*	⊢
	: , : , : , :
48	instantiation	87, 194, 171, 71, 111, 133, 108, 105, 73, 98	, , ,  ⊢
	: , : , : , : , : , : , :
49	instantiation	87, 171, 194, 72, 111, 133, 108, 105, 73, 98	, , ,  ⊢
	: , : , : , : , : , : , :
50	instantiation	175	⊢
	: , :
51	instantiation	86	⊢
	: , : , : , : , :
52	instantiation	74, 111, 155, 75*, 170*	⊢
	: , : , :
53	instantiation	175	⊢
	: , :
54	instantiation	175	⊢
	: , :
55	instantiation	76, 108, 182, 77, 78, 79*, 80*, 81*	⊢
	: , : , : , :
56	theorem		⊢
	proveit.logic.equality.sub_right_side_into
57	instantiation	104, 82, 98	, ,  ⊢
	: , :
58	instantiation	83, 88, 189, 194, 90, 84, 133, 105, 98	, ,  ⊢
	: , : , : , : , : , :
59	instantiation	104, 95, 96	⊢
	: , :
60	instantiation	106	⊢
	: , : , :
61	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
62	instantiation	129, 185	⊢
	:
63	instantiation	178, 128, 182, 85*	⊢
	: , :
64	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
65	instantiation	86	⊢
	: , : , : , : , :
66	instantiation	87, 172, 189, 88, 89, 94, 90, 95, 96, 133, 105, 98, 97	, , ,  ⊢
	: , : , : , : , : , : , :
67	instantiation	91, 189, 92, 93, 94, 95, 96, 133, 97, 105, 98, 99*	, , ,  ⊢
	: , : , : , : , : , :
68	theorem		⊢
	proveit.numbers.exponentiation.sqrt_complex_closure
69	instantiation	150, 177	⊢
	:
70	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
71	instantiation	100	⊢
	: , : , : , :
72	instantiation	100	⊢
	: , : , : , :
73	instantiation	107, 182, 109, 110	⊢
	: , :
74	theorem		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
75	instantiation	132, 111	⊢
	:
76	theorem		⊢
	proveit.numbers.division.prod_of_fracs
77	instantiation	192, 102, 101	⊢
	: , : , :
78	instantiation	192, 102, 103	⊢
	: , : , :
79	instantiation	150, 108	⊢
	:
80	instantiation	181, 108	⊢
	:
81	instantiation	176, 109	⊢
	:
82	instantiation	104, 133, 105	,  ⊢
	: , :
83	theorem		⊢
	proveit.numbers.multiplication.disassociation
84	instantiation	175	⊢
	: , :
85	instantiation	181, 128	⊢
	:
86	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
87	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
88	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
89	instantiation	106	⊢
	: , : , :
90	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
91	theorem		⊢
	proveit.numbers.multiplication.association
92	instantiation	175	⊢
	: , :
93	instantiation	175	⊢
	: , :
94	instantiation	175	⊢
	: , :
95	instantiation	107, 108, 109, 110	⊢
	: , :
96	instantiation	112, 111, 177	⊢
	: , :
97	instantiation	112, 133, 113	⊢
	: , :
98	instantiation	192, 184, 114	⊢
	: , : , :
99	instantiation	115, 133, 185, 116, 117, 118*, 119*	⊢
	: , : , :
100	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
101	instantiation	192, 121, 120	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
103	instantiation	192, 121, 122	⊢
	: , : , :
104	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
105	instantiation	192, 184, 123	⊢
	: , : , :
106	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
107	theorem		⊢
	proveit.numbers.division.div_complex_closure
108	instantiation	192, 184, 124	⊢
	: , : , :
109	instantiation	192, 184, 125	⊢
	: , : , :
110	instantiation	173, 157	⊢
	:
111	instantiation	192, 184, 126	⊢
	: , : , :
112	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
113	instantiation	127, 128	⊢
	:
114	assumption		⊢
115	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
116	instantiation	129, 146	⊢
	:
117	instantiation	130, 131	⊢
	:
118	instantiation	132, 133	⊢
	:
119	instantiation	134, 191, 135, 186, 136*, 137*, 138*	⊢
	: , : , : , :
120	instantiation	192, 140, 139	⊢
	: , : , :
121	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
122	instantiation	192, 140, 141	⊢
	: , : , :
123	instantiation	192, 162, 142	⊢
	: , : , :
124	instantiation	192, 187, 143	⊢
	: , : , :
125	instantiation	192, 187, 144	⊢
	: , : , :
126	instantiation	192, 162, 145	⊢
	: , : , :
127	theorem		⊢
	proveit.numbers.negation.complex_closure
128	instantiation	192, 184, 146	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.negation.real_closure
130	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
131	instantiation	192, 147, 163	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
133	instantiation	192, 184, 148	⊢
	: , : , :
134	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
135	instantiation	149, 191	⊢
	:
136	instantiation	150, 182	⊢
	:
137	instantiation	151, 182, 177, 161	⊢
	: , :
138	instantiation	152, 153, 154	⊢
	: , : , :
139	instantiation	192, 156, 155	⊢
	: , : , :
140	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
141	instantiation	192, 156, 157	⊢
	: , : , :
142	assumption		⊢
143	instantiation	192, 190, 158	⊢
	: , : , :
144	instantiation	192, 190, 159	⊢
	: , : , :
145	assumption		⊢
146	instantiation	160, 185, 180, 161	⊢
	: , :
147	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_neg_within_real_nonzero
148	instantiation	192, 162, 163	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.negation.int_closure
150	theorem		⊢
	proveit.numbers.division.frac_one_denom
151	theorem		⊢
	proveit.numbers.division.neg_frac_neg_numerator
152	axiom		⊢
	proveit.logic.equality.equals_transitivity
153	instantiation	164, 189, 165, 166, 167, 168	⊢
	: , : , : , :
154	instantiation	169, 182, 177, 170	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
156	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
157	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
158	instantiation	192, 193, 171	⊢
	: , : , :
159	instantiation	192, 193, 172	⊢
	: , : , :
160	theorem		⊢
	proveit.numbers.division.div_real_closure
161	instantiation	173, 174	⊢
	:
162	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_neg_within_real
163	assumption		⊢
164	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
165	instantiation	175	⊢
	: , :
166	instantiation	175	⊢
	: , :
167	instantiation	176, 177	⊢
	:
168	instantiation	178, 182, 179*	⊢
	: , :
169	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
170	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
171	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
172	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
173	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
174	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
175	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
176	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
177	instantiation	192, 184, 180	⊢
	: , : , :
178	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
179	instantiation	181, 182	⊢
	:
180	instantiation	192, 187, 183	⊢
	: , : , :
181	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
182	instantiation	192, 184, 185	⊢
	: , : , :
183	instantiation	192, 190, 186	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
185	instantiation	192, 187, 188	⊢
	: , : , :
186	instantiation	192, 193, 189	⊢
	: , : , :
187	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
188	instantiation	192, 190, 191	⊢
	: , : , :
189	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
190	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
191	instantiation	192, 193, 194	⊢
	: , : , :
192	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
193	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
194	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements