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, 87, 88, 4	⊢
	: , : , : , :
2	generalization	5	⊢
3	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
4	instantiation	6, 7, 58, 73, 8, 9*, 10*	⊢
	: , : , :
5	instantiation	30, 11	,  ⊢
	: , :
6	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
7	instantiation	100, 84, 12	⊢
	: , : , :
8	instantiation	13, 102	⊢
	:
9	instantiation	17, 14, 15, 16	⊢
	: , : , : , :
10	instantiation	17, 18, 19, 20	⊢
	: , : , : , :
11	instantiation	52, 21, 22	,  ⊢
	: , : , :
12	instantiation	100, 92, 23	⊢
	: , : , :
13	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
14	instantiation	52, 24, 25	⊢
	: , : , :
15	instantiation	26, 56, 65, 66, 27	⊢
	: , : , :
16	instantiation	76	⊢
	:
17	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
18	instantiation	52, 28, 29	⊢
	: , : , :
19	instantiation	76	⊢
	:
20	instantiation	30, 31	⊢
	: , :
21	instantiation	59, 60, 32, 89, 62, 33, 36, 34, 65, 50	,  ⊢
	: , : , : , : , : , :
22	instantiation	35, 89, 60, 62, 36, 50, 65	,  ⊢
	: , : , : , : , : , : , : , :
23	instantiation	93, 94, 80	⊢
	: , :
24	instantiation	59, 89, 99, 60, 42, 62, 50, 63	⊢
	: , : , : , : , : , :
25	instantiation	52, 37, 38	⊢
	: , : , :
26	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
27	instantiation	39, 40, 41	⊢
	: , : , :
28	instantiation	59, 89, 99, 60, 42, 62, 65, 63, 50	⊢
	: , : , : , : , : , :
29	instantiation	64, 65, 50, 67	⊢
	: , : , :
30	theorem		⊢
	proveit.logic.equality.equals_reversal
31	instantiation	43, 50	⊢
	:
32	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
33	instantiation	44	⊢
	: , : , :
34	instantiation	45, 50	⊢
	:
35	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
36	instantiation	100, 74, 46	,  ⊢
	: , : , :
37	instantiation	47, 89, 60, 62, 50, 63	⊢
	: , : , : , : , : , : , :
38	instantiation	48, 60, 99, 89, 62, 49, 50, 63, 51*	⊢
	: , : , : , : , : , :
39	theorem		⊢
	proveit.logic.equality.sub_right_side_into
40	instantiation	52, 53, 54	⊢
	: , : , :
41	instantiation	55, 65, 56	⊢
	: , :
42	instantiation	71	⊢
	: , :
43	theorem		⊢
	proveit.numbers.addition.elim_zero_left
44	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
45	theorem		⊢
	proveit.numbers.negation.complex_closure
46	instantiation	100, 84, 57	,  ⊢
	: , : , :
47	theorem		⊢
	proveit.numbers.addition.leftward_commutation
48	theorem		⊢
	proveit.numbers.addition.association
49	instantiation	71	⊢
	: , :
50	instantiation	100, 74, 58	⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
52	axiom		⊢
	proveit.logic.equality.equals_transitivity
53	instantiation	59, 89, 99, 60, 61, 62, 65, 63, 66	⊢
	: , : , : , : , : , :
54	instantiation	64, 65, 66, 67	⊢
	: , : , :
55	theorem		⊢
	proveit.numbers.addition.commutation
56	instantiation	100, 74, 68	⊢
	: , : , :
57	instantiation	100, 92, 69	,  ⊢
	: , : , :
58	instantiation	100, 84, 70	⊢
	: , : , :
59	theorem		⊢
	proveit.numbers.addition.disassociation
60	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
61	instantiation	71	⊢
	: , :
62	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
63	instantiation	100, 74, 72	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
65	instantiation	100, 74, 73	⊢
	: , : , :
66	instantiation	100, 74, 75	⊢
	: , : , :
67	instantiation	76	⊢
	:
68	instantiation	100, 84, 77	⊢
	: , : , :
69	instantiation	100, 78, 79	,  ⊢
	: , : , :
70	instantiation	100, 92, 80	⊢
	: , : , :
71	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
72	instantiation	100, 84, 81	⊢
	: , : , :
73	instantiation	82, 83, 102	⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
75	instantiation	100, 84, 85	⊢
	: , : , :
76	axiom		⊢
	proveit.logic.equality.equals_reflexivity
77	instantiation	100, 92, 87	⊢
	: , : , :
78	instantiation	86, 87, 88	⊢
	: , :
79	assumption		⊢
80	instantiation	100, 98, 89	⊢
	: , : , :
81	instantiation	100, 92, 94	⊢
	: , : , :
82	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
83	instantiation	90, 91	⊢
	: , :
84	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
85	instantiation	100, 92, 95	⊢
	: , : , :
86	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
87	instantiation	93, 94, 95	⊢
	: , :
88	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
89	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
90	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
91	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
92	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
93	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
94	instantiation	96, 97	⊢
	:
95	instantiation	100, 98, 99	⊢
	: , : , :
96	theorem		⊢
	proveit.numbers.negation.int_closure
97	instantiation	100, 101, 102	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
99	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
100	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
101	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
102	assumption		⊢
*equality replacement requirements