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