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