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, 4, 5, 143	⊢
	: , : , : , : , : , :
2	instantiation	15, 6, 7	⊢
	: , :
3	theorem		⊢
	proveit.logic.booleans.quantification.existence.skolem_elim
4	instantiation	8	⊢
	: , :
5	instantiation	8	⊢
	: , :
6	instantiation	9, 86	⊢
	:
7	generalization	10	⊢
8	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
9	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.reduced_nat_pos_ratio
10	deduction	11	, ,  ⊢
11	instantiation	12, 13, 14	, , ,  ⊢
	:
12	theorem		⊢
	proveit.logic.booleans.negation.negation_contradiction
13	instantiation	15, 34, 16	, , ,  ⊢
	: , :
14	instantiation	17, 143, 18	, ,  ⊢
	:
15	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
16	instantiation	35, 19, 67, 20	, , ,  ⊢
	: , :
17	instantiation	21, 123, 146, 22	, ,  ⊢
	: , :
18	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
19	instantiation	141, 46, 146	⊢
	: , : , :
20	instantiation	23, 41, 24, 25, 43	, , ,  ⊢
	: , : , :
21	theorem		⊢
	proveit.numbers.divisibility.GCD_one_def
22	instantiation	26, 71	⊢
	: , :
23	theorem		⊢
	proveit.numbers.divisibility.common_factor_elimination
24	instantiation	141, 136, 27	⊢
	: , : , :
25	instantiation	78, 28, 29	, , ,  ⊢
	: , : , :
26	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
27	instantiation	144, 145, 47	⊢
	: , : , :
28	instantiation	30, 31, 39	, , ,  ⊢
	: , : , :
29	instantiation	32, 41	⊢
	:
30	theorem		⊢
	proveit.logic.equality.sub_left_side_into
31	instantiation	33, 67, 36, 143, 34	, , ,  ⊢
	: , : , :
32	theorem		⊢
	proveit.numbers.exponentiation.square_expansion
33	theorem		⊢
	proveit.numbers.divisibility.common_exponent_introduction
34	instantiation	35, 36, 67, 37	, , ,  ⊢
	: , :
35	theorem		⊢
	proveit.numbers.divisibility.even__if__power_is_even
36	instantiation	141, 46, 123	⊢
	: , : , :
37	instantiation	78, 38, 39	, , ,  ⊢
	: , : , :
38	instantiation	40, 41, 42, 43	⊢
	: , :
39	instantiation	78, 44, 45	, , ,  ⊢
	: , : , :
40	theorem		⊢
	proveit.numbers.divisibility.left_factor_divisibility
41	instantiation	141, 136, 49	⊢
	: , : , :
42	instantiation	141, 46, 47	⊢
	: , : , :
43	instantiation	77, 143	⊢
	:
44	instantiation	48, 49, 50, 114, 51	, , ,  ⊢
	: , : , :
45	instantiation	52, 53, 130, 143, 54*	,  ⊢
	: , : , :
46	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
47	instantiation	55, 56, 88	⊢
	: , :
48	theorem		⊢
	proveit.numbers.exponentiation.exp_eq_real
49	instantiation	141, 124, 57	⊢
	: , : , :
50	instantiation	58, 63, 137	,  ⊢
	: , :
51	instantiation	59, 137, 63, 60, 61, 62*	, , ,  ⊢
	: , : , :
52	theorem		⊢
	proveit.numbers.exponentiation.posnat_power_of_product
53	instantiation	141, 136, 63	⊢
	: , : , :
54	instantiation	64, 106, 65*	⊢
	:
55	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
56	instantiation	141, 66, 146	⊢
	: , : , :
57	instantiation	141, 131, 67	⊢
	: , : , :
58	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
59	theorem		⊢
	proveit.numbers.multiplication.right_mult_eq_real
60	instantiation	68, 114, 137, 69	,  ⊢
	: , :
61	instantiation	70, 71	⊢
	: , :
62	instantiation	78, 72, 73	,  ⊢
	: , : , :
63	instantiation	141, 124, 74	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.exponentiation.square_abs_rational_simp
65	instantiation	75, 143, 76	⊢
	: , :
66	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
67	instantiation	141, 138, 88	⊢
	: , : , :
68	theorem		⊢
	proveit.numbers.division.div_real_closure
69	instantiation	77, 146	⊢
	:
70	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
71	assumption		⊢
72	instantiation	78, 79, 80	,  ⊢
	: , : , :
73	instantiation	81, 82, 83, 84	⊢
	: , : , : , :
74	instantiation	141, 85, 86	⊢
	: , : , :
75	theorem		⊢
	proveit.numbers.exponentiation.nth_power_of_nth_root
76	instantiation	87, 88	⊢
	:
77	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
78	theorem		⊢
	proveit.logic.equality.sub_right_side_into
79	instantiation	89, 103, 104, 90, 91	,  ⊢
	: , : , : , : , :
80	instantiation	111, 92, 93	⊢
	: , : , :
81	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
82	instantiation	120, 94	⊢
	: , : , :
83	instantiation	120, 95	⊢
	: , : , :
84	instantiation	129, 103	⊢
	:
85	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
86	instantiation	96, 97	⊢
	:
87	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
88	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
89	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
90	instantiation	141, 99, 98	⊢
	: , : , :
91	instantiation	141, 99, 100	⊢
	: , : , :
92	instantiation	120, 101	⊢
	: , : , :
93	instantiation	120, 102	⊢
	: , : , :
94	instantiation	122, 103	⊢
	:
95	instantiation	122, 104	⊢
	:
96	theorem		⊢
	proveit.numbers.absolute_value.abs_rational_nonzero_closure
97	instantiation	105, 106, 107	⊢
	:
98	instantiation	141, 108, 127	⊢
	: , : , :
99	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
100	instantiation	141, 108, 109	⊢
	: , : , :
101	instantiation	120, 110	⊢
	: , : , :
102	instantiation	111, 112, 113	⊢
	: , : , :
103	instantiation	141, 136, 114	⊢
	: , : , :
104	instantiation	141, 136, 115	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
106	assumption		⊢
107	instantiation	116, 128, 117	⊢
	: , :
108	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
109	instantiation	141, 134, 118	⊢
	: , : , :
110	instantiation	119, 130	⊢
	:
111	axiom		⊢
	proveit.logic.equality.equals_transitivity
112	instantiation	120, 121	⊢
	: , : , :
113	instantiation	122, 130	⊢
	:
114	instantiation	144, 145, 123	⊢
	: , : , :
115	instantiation	141, 124, 125	⊢
	: , : , :
116	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
117	instantiation	126, 127, 128	⊢
	: , :
118	instantiation	141, 142, 146	⊢
	: , : , :
119	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
120	axiom		⊢
	proveit.logic.equality.substitution
121	instantiation	129, 130	⊢
	:
122	theorem		⊢
	proveit.numbers.division.frac_one_denom
123	assumption		⊢
124	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
125	instantiation	141, 131, 132	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
127	instantiation	141, 134, 133	⊢
	: , : , :
128	instantiation	141, 134, 135	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
130	instantiation	141, 136, 137	⊢
	: , : , :
131	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
132	instantiation	141, 138, 139	⊢
	: , : , :
133	instantiation	141, 142, 140	⊢
	: , : , :
134	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
135	instantiation	141, 142, 143	⊢
	: , : , :
136	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
137	instantiation	144, 145, 146	⊢
	: , : , :
138	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
139	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
140	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
141	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
142	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
143	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
144	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
145	instantiation	147, 148	⊢
	: , :
146	assumption		⊢
147	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
148	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements