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