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