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, 5	⊢
	: , : , : , :
1	theorem		⊢
	proveit.core_expr_types.operations.operands_substitution_via_tuple
2	instantiation	195, 38, 194	⊢
	: , : , :
3	instantiation	94, 6	⊢
	: , : , :
4	instantiation	94, 7	⊢
	: , : , :
5	instantiation	27, 186, 11, 8, 9, 10*	⊢
	: , : , : , : , : , :
6	instantiation	27, 177, 11, 12, 13, 14*	⊢
	: , : , : , : , : , :
7	instantiation	135, 15, 16	⊢
	: , : , :
8	instantiation	132, 17	⊢
	: , :
9	instantiation	132, 18	⊢
	: , :
10	instantiation	149, 150, 187, 197, 153, 19, 20, 157, 156	,  ⊢
	: , : , : , : , : , :
11	instantiation	21, 22, 23	⊢
	: , :
12	instantiation	132, 24	⊢
	: , :
13	instantiation	132, 25	⊢
	: , :
14	instantiation	135, 26, 125	,  ⊢
	: , : , :
15	instantiation	27, 139, 28, 29, 30	⊢
	: , : , : , : , : , :
16	modus ponens	31, 32	⊢
17	instantiation	135, 33, 34	⊢
	: , : , :
18	instantiation	135, 35, 36	⊢
	: , : , :
19	instantiation	161	⊢
	: , :
20	instantiation	195, 173, 37	,  ⊢
	: , : , :
21	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
22	instantiation	195, 38, 39	⊢
	: , : , :
23	instantiation	40, 41	⊢
	:
24	instantiation	135, 42, 43	⊢
	: , : , :
25	instantiation	135, 44, 45	⊢
	: , : , :
26	instantiation	149, 150, 187, 197, 153, 142, 145, 154, 156	,  ⊢
	: , : , : , : , : , :
27	theorem		⊢
	proveit.core_expr_types.tuples.shift_equivalence
28	instantiation	46, 47, 48	⊢
	:
29	instantiation	132, 49	⊢
	: , :
30	instantiation	132, 50	⊢
	: , :
31	instantiation	51, 192, 190	⊢
	: , : , : , : , :
32	generalization	52	⊢
33	instantiation	94, 55	⊢
	: , : , :
34	instantiation	135, 53, 54	⊢
	: , : , :
35	instantiation	94, 55	⊢
	: , : , :
36	instantiation	63, 166	⊢
	:
37	instantiation	195, 181, 56	,  ⊢
	: , : , :
38	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
39	instantiation	57, 197, 150, 153, 58	⊢
	: , : , : , : , :
40	theorem		⊢
	proveit.numbers.negation.nat_closure
41	instantiation	59, 139, 60	⊢
	:
42	instantiation	94, 115	⊢
	: , : , :
43	instantiation	135, 61, 62	⊢
	: , : , :
44	instantiation	94, 115	⊢
	: , : , :
45	instantiation	63, 156	⊢
	:
46	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
47	instantiation	185, 64, 65	⊢
	: , :
48	instantiation	66, 67	⊢
	: , :
49	instantiation	135, 68, 69	⊢
	: , : , :
50	instantiation	118, 156, 70, 166, 71	⊢
	: , : , :
51	theorem		⊢
	proveit.core_expr_types.tuples.range_fn_transformation
52	instantiation	135, 72, 73	,  ⊢
	: , : , :
53	instantiation	149, 150, 187, 197, 153, 120, 154, 166	⊢
	: , : , : , : , : , :
54	instantiation	74, 197, 187, 150, 75, 153, 154, 166, 133*	⊢
	: , : , : , : , : , :
55	instantiation	134, 166	⊢
	:
56	instantiation	195, 188, 76	,  ⊢
	: , : , :
57	theorem		⊢
	proveit.numbers.addition.add_nat_pos_from_nonneg
58	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
59	theorem		⊢
	proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
60	instantiation	82, 162, 174, 164, 77, 78*, 79*	⊢
	: , : , :
61	instantiation	149, 150, 187, 197, 153, 120, 154, 166, 156	⊢
	: , : , : , : , : , :
62	instantiation	80, 156, 166, 147	⊢
	: , : , :
63	theorem		⊢
	proveit.numbers.addition.elim_zero_left
64	instantiation	195, 193, 81	⊢
	: , : , :
65	instantiation	191, 126	⊢
	:
66	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
67	instantiation	82, 83, 84, 164, 85, 86*, 87*	⊢
	: , : , :
68	instantiation	94, 88	⊢
	: , : , :
69	instantiation	135, 89, 90	⊢
	: , : , :
70	instantiation	195, 173, 91	⊢
	: , : , :
71	instantiation	135, 92, 93	⊢
	: , : , :
72	instantiation	94, 95	,  ⊢
	: , : , :
73	instantiation	135, 96, 97	,  ⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.addition.association
75	instantiation	161	⊢
	: , :
76	instantiation	195, 98, 99	,  ⊢
	: , : , :
77	instantiation	100, 194	⊢
	:
78	instantiation	101, 166, 154	⊢
	: , :
79	instantiation	102, 156, 147	⊢
	: , :
80	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_31
81	instantiation	103, 104	⊢
	: , :
82	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
83	instantiation	195, 181, 105	⊢
	: , : , :
84	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
85	instantiation	106, 107	⊢
	: , :
86	instantiation	135, 108, 109	⊢
	: , : , :
87	instantiation	110, 111, 112, 113	⊢
	: , : , : , :
88	instantiation	114, 154, 166, 115*	⊢
	: , :
89	instantiation	135, 116, 117	⊢
	: , : , :
90	instantiation	118, 166, 155, 133	⊢
	: , : , :
91	instantiation	195, 181, 119	⊢
	: , : , :
92	instantiation	149, 197, 187, 150, 120, 153, 156, 154, 166	⊢
	: , : , : , : , : , :
93	instantiation	146, 156, 166, 147	⊢
	: , : , :
94	axiom		⊢
	proveit.logic.equality.substitution
95	instantiation	149, 197, 187, 150, 120, 153, 145, 154, 166	,  ⊢
	: , : , : , : , : , :
96	instantiation	149, 150, 121, 187, 153, 122, 123, 145, 154, 166, 157, 156	,  ⊢
	: , : , : , : , : , :
97	instantiation	135, 124, 125	,  ⊢
	: , : , :
98	instantiation	189, 126, 192	⊢
	: , :
99	assumption		⊢
100	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
101	theorem		⊢
	proveit.numbers.addition.commutation
102	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
103	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
104	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
105	instantiation	195, 188, 126	⊢
	: , : , :
106	theorem		⊢
	proveit.numbers.ordering.relax_less
107	instantiation	127, 194	⊢
	:
108	instantiation	149, 197, 187, 150, 151, 153, 128, 154, 155	⊢
	: , : , : , : , : , :
109	instantiation	129, 150, 187, 153, 151, 154, 155	⊢
	: , : , : , :
110	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
111	instantiation	135, 130, 131	⊢
	: , : , :
112	instantiation	159	⊢
	:
113	instantiation	132, 133	⊢
	: , :
114	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
115	instantiation	134, 156	⊢
	:
116	instantiation	135, 136, 137	⊢
	: , : , :
117	instantiation	138, 150, 197, 153, 156, 155, 157	⊢
	: , : , : , : , : , : , : , :
118	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
119	instantiation	195, 188, 139	⊢
	: , : , :
120	instantiation	161	⊢
	: , :
121	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
122	instantiation	140	⊢
	: , : , :
123	instantiation	161	⊢
	: , :
124	instantiation	141, 187, 150, 197, 142, 153, 145, 154, 166, 156, 143	,  ⊢
	: , : , : , : , : , : , : , :
125	instantiation	144, 156, 145, 147	,  ⊢
	: , : , :
126	instantiation	185, 177, 178	⊢
	: , :
127	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
128	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
129	theorem		⊢
	proveit.numbers.addition.elim_zero_any
130	instantiation	149, 197, 187, 150, 151, 153, 156, 154, 155	⊢
	: , : , : , : , : , :
131	instantiation	146, 156, 155, 147	⊢
	: , : , :
132	theorem		⊢
	proveit.logic.equality.equals_reversal
133	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
134	theorem		⊢
	proveit.numbers.negation.double_negation
135	axiom		⊢
	proveit.logic.equality.equals_transitivity
136	instantiation	149, 150, 187, 197, 153, 151, 154, 155, 148	⊢
	: , : , : , : , : , :
137	instantiation	149, 187, 150, 151, 152, 153, 154, 155, 156, 157	⊢
	: , : , : , : , : , :
138	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
139	instantiation	185, 177, 192	⊢
	: , :
140	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
141	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
142	instantiation	161	⊢
	: , :
143	instantiation	159	⊢
	:
144	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
145	instantiation	195, 173, 158	,  ⊢
	: , : , :
146	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
147	instantiation	159	⊢
	:
148	instantiation	195, 173, 160	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.addition.disassociation
150	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
151	instantiation	161	⊢
	: , :
152	instantiation	161	⊢
	: , :
153	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
154	instantiation	195, 173, 162	⊢
	: , : , :
155	instantiation	195, 173, 163	⊢
	: , : , :
156	instantiation	195, 173, 164	⊢
	: , : , :
157	instantiation	165, 166	⊢
	:
158	instantiation	195, 181, 167	,  ⊢
	: , : , :
159	axiom		⊢
	proveit.logic.equality.equals_reflexivity
160	instantiation	195, 181, 168	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
162	instantiation	195, 181, 169	⊢
	: , : , :
163	instantiation	195, 181, 170	⊢
	: , : , :
164	instantiation	171, 172, 194	⊢
	: , : , :
165	theorem		⊢
	proveit.numbers.negation.complex_closure
166	instantiation	195, 173, 174	⊢
	: , : , :
167	instantiation	195, 188, 175	,  ⊢
	: , : , :
168	instantiation	195, 188, 176	⊢
	: , : , :
169	instantiation	195, 188, 177	⊢
	: , : , :
170	instantiation	195, 188, 178	⊢
	: , : , :
171	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
172	instantiation	179, 180	⊢
	: , :
173	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
174	instantiation	195, 181, 182	⊢
	: , : , :
175	instantiation	195, 183, 184	,  ⊢
	: , : , :
176	instantiation	185, 190, 186	⊢
	: , :
177	instantiation	191, 190	⊢
	:
178	instantiation	195, 196, 187	⊢
	: , : , :
179	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
180	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
181	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
182	instantiation	195, 188, 192	⊢
	: , : , :
183	instantiation	189, 192, 190	⊢
	: , :
184	assumption		⊢
185	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
186	instantiation	191, 192	⊢
	:
187	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
188	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
189	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
190	instantiation	195, 193, 194	⊢
	: , : , :
191	theorem		⊢
	proveit.numbers.negation.int_closure
192	instantiation	195, 196, 197	⊢
	: , : , :
193	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
194	assumption		⊢
195	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
196	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
197	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements