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