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, 6, 7, 8	⊢
	: , : , : , : , : , :
1	theorem		⊢
	proveit.logic.booleans.conjunction.disassociate
2	reference	163	⊢
3	reference	23	⊢
4	reference	158	⊢
5	instantiation	123	⊢
	: , :
6	reference	56	⊢
7	instantiation	87, 9, 41, 10	⊢
	: , : , : , :
8	instantiation	11, 12, 13, 14, 51, 15, 16	⊢
	: , :
9	instantiation	120, 17, 56	⊢
	: , : , :
10	instantiation	64, 18	⊢
	: , :
11	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
12	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
13	instantiation	19	⊢
	: , : , : , :
14	instantiation	125	⊢
	:
15	modus ponens	20, 21	⊢
16	instantiation	125	⊢
	:
17	instantiation	22, 23	⊢
	: , : , :
18	instantiation	24, 25	⊢
	: , :
19	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
20	instantiation	26, 137, 138, 27	⊢
	: , : , : , :
21	generalization	28	⊢
22	theorem		⊢
	proveit.core_expr_types.tuples.range_len
23	instantiation	120, 29, 30	⊢
	: , : , :
24	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
25	instantiation	31, 32, 33	⊢
	:
26	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
27	instantiation	70, 34, 141, 129, 71, 35*, 36*	⊢
	: , : , :
28	instantiation	64, 37	,  ⊢
	: , :
29	instantiation	38, 39	⊢
	:
30	instantiation	87, 40, 41, 42	⊢
	: , : , : , :
31	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
32	instantiation	144, 152, 43	⊢
	: , :
33	instantiation	44, 71	⊢
	: , :
34	instantiation	161, 154, 45	⊢
	: , : , :
35	instantiation	87, 46, 47, 48	⊢
	: , : , : , :
36	instantiation	87, 49, 50, 51	⊢
	: , : , : , :
37	instantiation	93, 52, 53	,  ⊢
	: , : , :
38	theorem		⊢
	proveit.numbers.negation.nat_closure
39	instantiation	54, 57, 55	⊢
	:
40	instantiation	98, 112, 133, 99*	⊢
	: , :
41	instantiation	125	⊢
	:
42	instantiation	64, 56	⊢
	: , :
43	instantiation	151, 153	⊢
	:
44	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
45	instantiation	161, 159, 57	⊢
	: , : , :
46	instantiation	93, 58, 59	⊢
	: , : , :
47	instantiation	60, 96, 118, 143, 61	⊢
	: , : , :
48	instantiation	125	⊢
	:
49	instantiation	93, 62, 63	⊢
	: , : , :
50	instantiation	125	⊢
	:
51	instantiation	64, 65	⊢
	: , :
52	instantiation	108, 109, 103, 158, 111, 66, 69, 67, 118, 133	,  ⊢
	: , : , : , : , : , :
53	instantiation	68, 158, 109, 111, 69, 133, 118	,  ⊢
	: , : , : , : , : , : , : , :
54	theorem		⊢
	proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
55	instantiation	70, 124, 141, 129, 71, 72*, 73*	⊢
	: , : , :
56	instantiation	93, 74, 75	⊢
	: , : , :
57	instantiation	144, 145, 153	⊢
	: , :
58	instantiation	108, 158, 163, 109, 80, 111, 133, 112	⊢
	: , : , : , : , : , :
59	instantiation	93, 76, 77	⊢
	: , : , :
60	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
61	instantiation	120, 78, 79	⊢
	: , : , :
62	instantiation	108, 158, 163, 109, 80, 111, 118, 112, 133	⊢
	: , : , : , : , : , :
63	instantiation	113, 118, 133, 114	⊢
	: , : , :
64	theorem		⊢
	proveit.logic.equality.equals_reversal
65	instantiation	81, 133	⊢
	:
66	instantiation	119	⊢
	: , : , :
67	instantiation	142, 133	⊢
	:
68	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
69	instantiation	161, 149, 82	,  ⊢
	: , : , :
70	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
71	instantiation	83, 157	⊢
	:
72	instantiation	132, 133, 112	⊢
	: , :
73	instantiation	84, 118, 114	⊢
	: , :
74	instantiation	85, 86	⊢
	: , : , :
75	instantiation	87, 88, 89, 90	⊢
	: , : , : , :
76	instantiation	91, 158, 109, 111, 133, 112	⊢
	: , : , : , : , : , : , :
77	instantiation	105, 109, 163, 158, 111, 92, 133, 112, 131*	⊢
	: , : , : , : , : , :
78	instantiation	93, 94, 95	⊢
	: , : , :
79	instantiation	132, 118, 96	⊢
	: , :
80	instantiation	123	⊢
	: , :
81	theorem		⊢
	proveit.numbers.addition.elim_zero_left
82	instantiation	161, 154, 97	,  ⊢
	: , : , :
83	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
84	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
85	axiom		⊢
	proveit.logic.equality.substitution
86	instantiation	98, 112, 143, 99*	⊢
	: , :
87	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
88	instantiation	108, 158, 163, 100, 101, 118, 134, 133	⊢
	: , : , : , : , : , :
89	instantiation	102, 109, 103, 111, 104, 118, 134, 133	⊢
	: , : , : , :
90	instantiation	105, 158, 163, 109, 106, 111, 118, 134, 133, 107*	⊢
	: , : , : , : , : , :
91	theorem		⊢
	proveit.numbers.addition.leftward_commutation
92	instantiation	123	⊢
	: , :
93	axiom		⊢
	proveit.logic.equality.equals_transitivity
94	instantiation	108, 158, 163, 109, 110, 111, 118, 112, 143	⊢
	: , : , : , : , : , :
95	instantiation	113, 118, 143, 114	⊢
	: , : , :
96	instantiation	161, 149, 115	⊢
	: , : , :
97	instantiation	161, 159, 116	,  ⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
99	instantiation	117, 118	⊢
	:
100	instantiation	123	⊢
	: , :
101	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
102	theorem		⊢
	proveit.numbers.addition.elim_zero_any
103	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
104	instantiation	119	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.addition.association
106	instantiation	123	⊢
	: , :
107	instantiation	120, 121, 122	⊢
	: , : , :
108	theorem		⊢
	proveit.numbers.addition.disassociation
109	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
110	instantiation	123	⊢
	: , :
111	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
112	instantiation	161, 149, 124	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
114	instantiation	125	⊢
	:
115	instantiation	161, 154, 126	⊢
	: , : , :
116	instantiation	161, 127, 128	,  ⊢
	: , : , :
117	theorem		⊢
	proveit.numbers.negation.double_negation
118	instantiation	161, 149, 129	⊢
	: , : , :
119	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
120	theorem		⊢
	proveit.logic.equality.sub_right_side_into
121	instantiation	130, 133, 143, 131	⊢
	: , : , :
122	instantiation	132, 133, 134	⊢
	: , :
123	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
124	instantiation	161, 154, 135	⊢
	: , : , :
125	axiom		⊢
	proveit.logic.equality.equals_reflexivity
126	instantiation	161, 159, 137	⊢
	: , : , :
127	instantiation	136, 137, 138	⊢
	: , :
128	assumption		⊢
129	instantiation	139, 140, 157	⊢
	: , : , :
130	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
131	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
132	theorem		⊢
	proveit.numbers.addition.commutation
133	instantiation	161, 149, 141	⊢
	: , : , :
134	instantiation	142, 143	⊢
	:
135	instantiation	161, 159, 145	⊢
	: , : , :
136	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
137	instantiation	144, 145, 160	⊢
	: , :
138	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
139	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
140	instantiation	146, 147	⊢
	: , :
141	instantiation	161, 154, 148	⊢
	: , : , :
142	theorem		⊢
	proveit.numbers.negation.complex_closure
143	instantiation	161, 149, 150	⊢
	: , : , :
144	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
145	instantiation	151, 152	⊢
	:
146	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
147	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
148	instantiation	161, 159, 153	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
150	instantiation	161, 154, 155	⊢
	: , : , :
151	theorem		⊢
	proveit.numbers.negation.int_closure
152	instantiation	161, 156, 157	⊢
	: , : , :
153	instantiation	161, 162, 158	⊢
	: , : , :
154	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
155	instantiation	161, 159, 160	⊢
	: , : , :
156	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
157	assumption		⊢
158	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
159	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
160	instantiation	161, 162, 163	⊢
	: , : , :
161	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
162	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
163	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements