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