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	105	⊢
2	instantiation	93, 130, 161, 5, 21, 6, 7, 23	, , , ,  ⊢
	: , : , : , : , : , :
3	instantiation	8, 9, 10, 11	, ,  ⊢
	: , : , : , :
4	instantiation	122, 12, 13	, , , ,  ⊢
	: , : , :
5	instantiation	144	⊢
	: , :
6	instantiation	54, 76, 14	,  ⊢
	: , :
7	instantiation	54, 76, 15	,  ⊢
	: , :
8	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
9	instantiation	79, 16	,  ⊢
	: , : , :
10	instantiation	79, 17	,  ⊢
	: , : , :
11	instantiation	52, 18	, ,  ⊢
	: , :
12	instantiation	79, 19	, ,  ⊢
	: , : , :
13	instantiation	93, 130, 161, 133, 20, 134, 21, 22, 23, 24*	, , , ,  ⊢
	: , : , : , : , : , :
14	instantiation	105, 25, 26	,  ⊢
	: , : , :
15	instantiation	105, 27, 28	,  ⊢
	: , : , :
16	instantiation	122, 29, 30	,  ⊢
	: , : , :
17	instantiation	122, 31, 32	,  ⊢
	: , : , :
18	instantiation	33, 34, 35, 126, 36, 37	, ,  ⊢
	: , : , :
19	instantiation	122, 38, 39	, ,  ⊢
	: , : , :
20	instantiation	144	⊢
	: , :
21	instantiation	159, 149, 40	,  ⊢
	: , : , :
22	instantiation	54, 76, 41	, ,  ⊢
	: , :
23	instantiation	54, 76, 42	⊢
	: , :
24	instantiation	81, 117, 41, 42	, , ,  ⊢
	: , : , :
25	instantiation	141, 131, 43	,  ⊢
	: , :
26	instantiation	122, 44, 45	,  ⊢
	: , : , :
27	instantiation	141, 131, 46	,  ⊢
	: , :
28	instantiation	122, 47, 48	,  ⊢
	: , : , :
29	instantiation	79, 49	,  ⊢
	: , : , :
30	instantiation	52, 50	,  ⊢
	: , :
31	instantiation	79, 51	,  ⊢
	: , : , :
32	instantiation	52, 53	,  ⊢
	: , :
33	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
34	instantiation	54, 76, 83	⊢
	: , :
35	instantiation	54, 76, 84	⊢
	: , :
36	instantiation	55, 56, 57	⊢
	: , : , :
37	instantiation	75, 76, 84, 78	⊢
	: , :
38	instantiation	79, 58	,  ⊢
	: , : , :
39	instantiation	59, 117, 62, 110	, ,  ⊢
	: , : , :
40	instantiation	60, 61, 125	,  ⊢
	: , :
41	instantiation	141, 62, 110	, ,  ⊢
	: , :
42	instantiation	105, 63, 64	⊢
	: , : , :
43	instantiation	105, 65, 66	,  ⊢
	: , : , :
44	instantiation	132, 130, 91, 133, 67, 134, 131, 137, 110, 129	,  ⊢
	: , : , : , : , : , :
45	instantiation	132, 133, 161, 91, 134, 135, 67, 142, 143, 137, 110, 129	,  ⊢
	: , : , : , : , : , :
46	instantiation	105, 68, 69	,  ⊢
	: , : , :
47	instantiation	132, 130, 91, 133, 70, 134, 131, 137, 138, 110	,  ⊢
	: , : , : , : , : , :
48	instantiation	132, 133, 161, 91, 134, 135, 70, 142, 143, 137, 138, 110	,  ⊢
	: , : , : , : , : , :
49	instantiation	122, 71, 72	,  ⊢
	: , : , :
50	instantiation	74, 76, 83, 78	,  ⊢
	: , :
51	instantiation	93, 133, 94, 130, 134, 73, 142, 143, 137, 138, 110	,  ⊢
	: , : , : , : , : , :
52	theorem		⊢
	proveit.logic.equality.equals_reversal
53	instantiation	74, 76, 84, 78	,  ⊢
	: , :
54	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
55	theorem		⊢
	proveit.logic.equality.sub_left_side_into
56	instantiation	75, 76, 77, 78	⊢
	: , :
57	instantiation	79, 80	⊢
	: , : , :
58	instantiation	81, 117, 83, 84	,  ⊢
	: , : , :
59	theorem		⊢
	proveit.numbers.exponentiation.complex_power_of_complex_power
60	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
61	assumption		⊢
62	instantiation	82, 83, 84	,  ⊢
	: , :
63	instantiation	141, 131, 85	⊢
	: , :
64	instantiation	122, 86, 87	⊢
	: , : , :
65	instantiation	141, 88, 129	,  ⊢
	: , :
66	instantiation	132, 133, 161, 130, 134, 89, 137, 110, 129	,  ⊢
	: , : , : , : , : , :
67	instantiation	111	⊢
	: , : , :
68	instantiation	141, 121, 110	,  ⊢
	: , :
69	instantiation	132, 133, 161, 130, 134, 136, 137, 138, 110	,  ⊢
	: , : , : , : , : , :
70	instantiation	111	⊢
	: , : , :
71	instantiation	90, 91, 130, 133, 92, 134, 142, 143, 137, 110, 129	,  ⊢
	: , : , : , : , : , : , :
72	instantiation	93, 133, 94, 130, 134, 95, 142, 143, 137, 129, 110	,  ⊢
	: , : , : , : , : , :
73	instantiation	112	⊢
	: , : , : , :
74	instantiation	96, 146	⊢
	:
75	theorem		⊢
	proveit.numbers.exponentiation.exp_not_eq_zero
76	instantiation	159, 149, 97	⊢
	: , : , :
77	instantiation	105, 98, 99	⊢
	: , : , :
78	instantiation	100, 101	⊢
	:
79	axiom		⊢
	proveit.logic.equality.substitution
80	instantiation	102, 161, 130, 133, 135, 134, 142, 143, 137, 129	⊢
	: , : , : , : , : , : , :
81	theorem		⊢
	proveit.numbers.exponentiation.product_of_complex_powers
82	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
83	instantiation	105, 103, 104	⊢
	: , : , :
84	instantiation	105, 106, 107	⊢
	: , : , :
85	instantiation	141, 137, 109	⊢
	: , :
86	instantiation	132, 130, 161, 133, 108, 134, 131, 137, 109	⊢
	: , : , : , : , : , :
87	instantiation	132, 133, 161, 134, 135, 108, 142, 143, 137, 109	⊢
	: , : , : , : , : , :
88	instantiation	141, 137, 110	⊢
	: , :
89	instantiation	144	⊢
	: , :
90	theorem		⊢
	proveit.numbers.multiplication.rightward_commutation
91	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
92	instantiation	111	⊢
	: , : , :
93	theorem		⊢
	proveit.numbers.multiplication.association
94	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
95	instantiation	112	⊢
	: , : , : , :
96	theorem		⊢
	proveit.numbers.exponentiation.int_exp_of_exp
97	instantiation	159, 155, 117	⊢
	: , : , :
98	instantiation	141, 131, 113	⊢
	: , :
99	instantiation	122, 114, 115	⊢
	: , : , :
100	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
101	instantiation	159, 116, 117	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
103	instantiation	141, 131, 118	⊢
	: , :
104	instantiation	122, 119, 120	⊢
	: , : , :
105	theorem		⊢
	proveit.logic.equality.sub_right_side_into
106	instantiation	141, 131, 121	⊢
	: , :
107	instantiation	122, 123, 124	⊢
	: , : , :
108	instantiation	144	⊢
	: , :
109	instantiation	159, 149, 125	⊢
	: , : , :
110	instantiation	159, 149, 126	⊢
	: , : , :
111	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
112	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
113	instantiation	141, 129, 137	⊢
	: , :
114	instantiation	132, 130, 161, 133, 127, 134, 131, 129, 137	⊢
	: , : , : , : , : , :
115	instantiation	132, 133, 161, 134, 135, 127, 142, 143, 129, 137	⊢
	: , : , : , : , : , :
116	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
117	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
118	instantiation	141, 137, 129	⊢
	: , :
119	instantiation	132, 130, 161, 133, 128, 134, 131, 137, 129	⊢
	: , : , : , : , : , :
120	instantiation	132, 133, 161, 134, 135, 128, 142, 143, 137, 129	⊢
	: , : , : , : , : , :
121	instantiation	141, 137, 138	⊢
	: , :
122	axiom		⊢
	proveit.logic.equality.equals_transitivity
123	instantiation	132, 130, 161, 133, 136, 134, 131, 137, 138	⊢
	: , : , : , : , : , :
124	instantiation	132, 133, 161, 134, 135, 136, 142, 143, 137, 138	⊢
	: , : , : , : , : , :
125	assumption		⊢
126	instantiation	159, 153, 139	⊢
	: , : , :
127	instantiation	144	⊢
	: , :
128	instantiation	144	⊢
	: , :
129	instantiation	159, 149, 140	⊢
	: , : , :
130	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
131	instantiation	141, 142, 143	⊢
	: , :
132	theorem		⊢
	proveit.numbers.multiplication.disassociation
133	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
134	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
135	instantiation	144	⊢
	: , :
136	instantiation	144	⊢
	: , :
137	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
138	instantiation	159, 149, 145	⊢
	: , : , :
139	instantiation	159, 157, 146	⊢
	: , : , :
140	instantiation	159, 153, 147	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
142	instantiation	159, 149, 148	⊢
	: , : , :
143	instantiation	159, 149, 150	⊢
	: , : , :
144	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
145	instantiation	159, 155, 151	⊢
	: , : , :
146	assumption		⊢
147	instantiation	159, 157, 152	⊢
	: , : , :
148	instantiation	159, 153, 154	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
150	instantiation	159, 155, 156	⊢
	: , : , :
151	assumption		⊢
152	assumption		⊢
153	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
154	instantiation	159, 157, 158	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
156	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
157	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
158	instantiation	159, 160, 161	⊢
	: , : , :
159	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
160	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
161	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements