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	theorem		⊢
	proveit.logic.equality.equals_reversal
2	instantiation	84, 3, 4	⊢
	: , : , :
3	instantiation	94, 5	⊢
	: , : , :
4	instantiation	94, 6	⊢
	: , : , :
5	instantiation	84, 7, 8	⊢
	: , : , :
6	instantiation	84, 9, 10	⊢
	: , : , :
7	instantiation	94, 11	⊢
	: , : , :
8	instantiation	73, 100, 12, 13, 14*	⊢
	: , :
9	instantiation	94, 15	⊢
	: , : , :
10	instantiation	73, 100, 16, 17, 18*	⊢
	: , :
11	instantiation	94, 19	⊢
	: , : , :
12	instantiation	20, 115	⊢
	:
13	instantiation	24, 122, 21	⊢
	: , :
14	instantiation	84, 22, 23	⊢
	: , : , :
15	instantiation	94, 62	⊢
	: , : , :
16	instantiation	48, 115, 63	⊢
	: , :
17	instantiation	24, 122, 25	⊢
	: , :
18	instantiation	84, 26, 27	⊢
	: , : , :
19	instantiation	84, 28, 29	⊢
	: , : , :
20	theorem		⊢
	proveit.numbers.exponentiation.sqrt_complex_closure
21	instantiation	30, 31, 122	⊢
	: , :
22	instantiation	94, 32	⊢
	: , : , :
23	instantiation	36, 33	⊢
	:
24	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
25	instantiation	144, 34, 97	⊢
	: , : , :
26	instantiation	94, 35	⊢
	: , : , :
27	instantiation	36, 37	⊢
	:
28	instantiation	84, 38, 39	⊢
	: , : , :
29	instantiation	84, 40, 41	⊢
	: , : , :
30	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
31	instantiation	144, 130, 42	⊢
	: , : , :
32	instantiation	45, 115, 111, 46, 74, 43*	⊢
	: , : , :
33	instantiation	48, 115, 44	⊢
	: , :
34	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
35	instantiation	45, 115, 76, 46, 74, 47*	⊢
	: , : , :
36	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
37	instantiation	48, 115, 53	⊢
	: , :
38	instantiation	94, 49	⊢
	: , : , :
39	instantiation	94, 50	⊢
	: , : , :
40	instantiation	51, 90, 146, 134, 92, 52, 63, 103, 53	⊢
	: , : , : , : , : , :
41	instantiation	54, 63, 103, 55	⊢
	: , : , :
42	instantiation	144, 138, 141	⊢
	: , : , :
43	instantiation	56, 103, 100, 93*	⊢
	: , :
44	instantiation	144, 123, 57	⊢
	: , : , :
45	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
46	instantiation	144, 132, 58	⊢
	: , : , :
47	instantiation	84, 59, 60	⊢
	: , : , :
48	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
49	instantiation	73, 88, 115, 74, 61*	⊢
	: , :
50	instantiation	94, 62	⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.addition.disassociation
52	instantiation	101	⊢
	: , :
53	instantiation	78, 63	⊢
	:
54	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
55	instantiation	64	⊢
	:
56	theorem		⊢
	proveit.numbers.negation.pos_times_neg
57	instantiation	65, 111	⊢
	:
58	instantiation	144, 139, 66	⊢
	: , : , :
59	instantiation	67, 90, 146, 134, 92, 80, 103, 99, 68	⊢
	: , : , : , : , : , :
60	instantiation	69, 146, 90, 80, 92, 103, 99, 100, 70*	⊢
	: , : , : , : , :
61	instantiation	84, 71, 72	⊢
	: , : , :
62	instantiation	73, 99, 115, 74, 75*	⊢
	: , :
63	instantiation	144, 123, 76	⊢
	: , : , :
64	axiom		⊢
	proveit.logic.equality.equals_reflexivity
65	theorem		⊢
	proveit.numbers.negation.real_closure
66	instantiation	77, 127	⊢
	:
67	theorem		⊢
	proveit.numbers.multiplication.disassociation
68	instantiation	78, 100	⊢
	:
69	theorem		⊢
	proveit.numbers.multiplication.mult_neg_any
70	instantiation	79, 146, 90, 80, 92, 103, 99	⊢
	: , : , : , :
71	instantiation	94, 95	⊢
	: , : , :
72	instantiation	84, 81, 82	⊢
	: , : , :
73	theorem		⊢
	proveit.numbers.division.div_as_mult
74	instantiation	83, 143	⊢
	:
75	instantiation	84, 85, 86	⊢
	: , : , :
76	instantiation	144, 132, 87	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.negation.int_closure
78	theorem		⊢
	proveit.numbers.negation.complex_closure
79	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
80	instantiation	101	⊢
	: , :
81	instantiation	96, 88, 103	⊢
	: , :
82	instantiation	89, 134, 146, 90, 91, 92, 103, 99, 100, 93*	⊢
	: , : , : , : , : , :
83	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
84	axiom		⊢
	proveit.logic.equality.equals_transitivity
85	instantiation	94, 95	⊢
	: , : , :
86	instantiation	96, 99, 103	⊢
	: , :
87	instantiation	144, 128, 97	⊢
	: , : , :
88	instantiation	98, 99, 100	⊢
	: , :
89	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
90	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
91	instantiation	101	⊢
	: , :
92	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
93	instantiation	102, 103	⊢
	:
94	axiom		⊢
	proveit.logic.equality.substitution
95	instantiation	104, 105, 141, 106*	⊢
	: , :
96	theorem		⊢
	proveit.numbers.multiplication.commutation
97	instantiation	107, 129, 108	⊢
	: , :
98	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
99	instantiation	144, 123, 109	⊢
	: , : , :
100	instantiation	144, 123, 110	⊢
	: , : , :
101	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
102	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
103	instantiation	144, 123, 111	⊢
	: , : , :
104	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
105	instantiation	144, 112, 113	⊢
	: , : , :
106	instantiation	114, 115	⊢
	:
107	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
108	instantiation	144, 142, 118	⊢
	: , : , :
109	instantiation	116, 117, 118	⊢
	: , : , :
110	instantiation	144, 132, 119	⊢
	: , : , :
111	instantiation	144, 132, 120	⊢
	: , : , :
112	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
113	instantiation	144, 121, 122	⊢
	: , : , :
114	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
115	instantiation	144, 123, 124	⊢
	: , : , :
116	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
117	instantiation	125, 126	⊢
	: , :
118	assumption		⊢
119	instantiation	144, 139, 127	⊢
	: , : , :
120	instantiation	144, 128, 129	⊢
	: , : , :
121	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
122	instantiation	144, 130, 131	⊢
	: , : , :
123	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
124	instantiation	144, 132, 133	⊢
	: , : , :
125	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
126	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
127	instantiation	144, 145, 134	⊢
	: , : , :
128	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
129	instantiation	135, 136, 137	⊢
	: , :
130	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
131	instantiation	144, 138, 143	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
133	instantiation	144, 139, 140	⊢
	: , : , :
134	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
135	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
136	instantiation	144, 142, 141	⊢
	: , : , :
137	instantiation	144, 142, 143	⊢
	: , : , :
138	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
139	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
140	instantiation	144, 145, 146	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
142	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
143	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
144	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
145	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
146	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements