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