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	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , : , :
2	axiom		⊢
	proveit.core_expr_types.conditionals.condition_replacement
3	instantiation	4, 5, 6	⊢
	: , :
4	theorem		⊢
	proveit.logic.booleans.implication.iff_intro
5	deduction	7	⊢
6	deduction	8	⊢
7	instantiation	13, 18, 9, 10, 11, 12	⊢
	: , :
8	instantiation	13, 14, 15, 90, 84, 16, 17	,  ⊢
	: , :
9	instantiation	26	⊢
	: , : , :
10	instantiation	102, 103, 18, 104, 19, 21	⊢
	: , : , : , : , :
11	instantiation	102, 123, 129, 20, 21	⊢
	: , : , : , : , :
12	instantiation	102, 129, 123, 23, 21	⊢
	: , : , : , : , :
13	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
14	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
15	instantiation	22	⊢
	: , : , : , :
16	instantiation	102, 129, 103, 23, 104, 106	⊢
	: , : , : , : , :
17	instantiation	24, 54, 71, 90, 25	,  ⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
19	instantiation	26	⊢
	: , : , :
20	instantiation	115	⊢
	: , :
21	assumption		⊢
22	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
23	instantiation	115	⊢
	: , :
24	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalCO
25	instantiation	27, 28, 29	,  ⊢
	: , :
26	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
27	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
28	instantiation	44, 101, 54, 45, 30, 48, 31*, 49*	,  ⊢
	: , : , :
29	instantiation	32, 33, 34	,  ⊢
	: , : , :
30	instantiation	35, 95, 96, 84	,  ⊢
	: , : , :
31	instantiation	36, 89, 68	⊢
	:
32	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
33	instantiation	37, 38, 39	,  ⊢
	: , : , :
34	instantiation	40, 71, 41, 54, 42, 43*	⊢
	: , : , :
35	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
36	theorem		⊢
	proveit.numbers.division.frac_zero_numer
37	theorem		⊢
	proveit.logic.equality.sub_right_side_into
38	instantiation	44, 101, 45, 46, 47, 48, 49*	,  ⊢
	: , : , :
39	instantiation	50, 89, 59, 68, 51*	⊢
	: , : , :
40	theorem		⊢
	proveit.numbers.addition.strong_bound_via_right_term_bound
41	instantiation	52, 55	⊢
	:
42	instantiation	53, 54, 55, 56, 57*	⊢
	: , :
43	instantiation	58, 59	⊢
	:
44	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
45	instantiation	130, 113, 60	,  ⊢
	: , : , :
46	instantiation	130, 113, 61	⊢
	: , : , :
47	instantiation	62, 95, 96, 84	,  ⊢
	: , : , :
48	instantiation	63, 118	⊢
	:
49	instantiation	64, 65, 66	,  ⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.division.distribute_frac_through_subtract
51	instantiation	67, 89, 68	⊢
	:
52	theorem		⊢
	proveit.numbers.negation.real_closure
53	theorem		⊢
	proveit.numbers.negation.negated_strong_bound
54	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
55	instantiation	130, 113, 69	⊢
	: , : , :
56	instantiation	70, 81	⊢
	:
57	theorem		⊢
	proveit.numbers.negation.negated_zero
58	theorem		⊢
	proveit.numbers.addition.elim_zero_right
59	instantiation	130, 100, 71	⊢
	: , : , :
60	instantiation	130, 121, 72	,  ⊢
	: , : , :
61	instantiation	130, 121, 96	⊢
	: , : , :
62	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
63	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
64	axiom		⊢
	proveit.logic.equality.equals_transitivity
65	instantiation	73, 74, 75, 78, 76*	,  ⊢
	: , : , :
66	instantiation	77, 78	⊢
	:
67	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
68	instantiation	79, 118	⊢
	:
69	instantiation	130, 80, 81	⊢
	: , : , :
70	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
71	instantiation	130, 113, 82	⊢
	: , : , :
72	instantiation	130, 83, 84	,  ⊢
	: , : , :
73	theorem		⊢
	proveit.numbers.division.frac_cancel_left
74	instantiation	130, 86, 85	⊢
	: , : , :
75	instantiation	130, 86, 87	⊢
	: , : , :
76	instantiation	88, 89	⊢
	:
77	theorem		⊢
	proveit.numbers.division.frac_one_denom
78	instantiation	130, 100, 90	⊢
	: , : , :
79	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
80	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
81	instantiation	91, 92, 93	⊢
	: , :
82	instantiation	130, 121, 117	⊢
	: , : , :
83	instantiation	94, 95, 96	⊢
	: , :
84	instantiation	102, 123, 106	⊢
	: , : , : , : , :
85	instantiation	130, 98, 97	⊢
	: , : , :
86	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
87	instantiation	130, 98, 99	⊢
	: , : , :
88	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
89	instantiation	130, 100, 101	⊢
	: , : , :
90	instantiation	102, 103, 129, 104, 105, 106	⊢
	: , : , : , : , :
91	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
92	instantiation	130, 107, 120	⊢
	: , : , :
93	instantiation	130, 107, 118	⊢
	: , : , :
94	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
95	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
96	instantiation	108, 122, 109	⊢
	: , :
97	instantiation	130, 111, 110	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
99	instantiation	130, 111, 112	⊢
	: , : , :
100	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
101	instantiation	130, 113, 114	⊢
	: , : , :
102	theorem		⊢
	proveit.logic.booleans.conjunction.any_from_and
103	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
104	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
105	instantiation	115	⊢
	: , :
106	assumption		⊢
107	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
108	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
109	instantiation	116, 117	⊢
	:
110	instantiation	130, 119, 118	⊢
	: , : , :
111	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
112	instantiation	130, 119, 120	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
114	instantiation	130, 121, 122	⊢
	: , : , :
115	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
116	theorem		⊢
	proveit.numbers.negation.int_closure
117	instantiation	130, 128, 123	⊢
	: , : , :
118	instantiation	124, 129, 127	⊢
	: , :
119	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
120	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
121	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
122	instantiation	125, 126, 127	⊢
	: , :
123	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
124	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
125	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
126	instantiation	130, 128, 129	⊢
	: , : , :
127	instantiation	130, 131, 132	⊢
	: , : , :
128	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
129	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
130	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
131	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
132	assumption		⊢
*equality replacement requirements