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