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