logo

Show the Proof

In [1]:
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
Out[1]:
 step typerequirementsstatement
0instantiation1, 2, 3, 4  ⊢  
  : , :
1theorem  ⊢  
 proveit.logic.booleans.implication.modus_tollens_denial
2instantiation5  ⊢  
  :
3deduction6  ⊢  
4theorem  ⊢  
 proveit.logic.booleans.negation.not_false
5theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_membership_is_bool
6modus ponens7, 8  ⊢  
7instantiation9, 10, 11, 149  ⊢  
  : , : , : , : , : , :
8instantiation21, 12, 13  ⊢  
  : , :
9theorem  ⊢  
 proveit.logic.booleans.quantification.existence.skolem_elim
10instantiation14  ⊢  
  : , :
11instantiation14  ⊢  
  : , :
12instantiation15, 92  ⊢  
  :
13generalization16  ⊢  
14theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
15theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.reduced_nat_pos_ratio
16deduction17, ,  ⊢  
17instantiation18, 19, 20, , ,  ⊢  
  :
18theorem  ⊢  
 proveit.logic.booleans.negation.negation_contradiction
19instantiation21, 40, 22, , ,  ⊢  
  : , :
20instantiation23, 149, 24, ,  ⊢  
  :
21theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
22instantiation41, 25, 73, 26, , ,  ⊢  
  : , :
23instantiation27, 129, 152, 28, ,  ⊢  
  : , :
24theorem  ⊢  
 proveit.numbers.numerals.decimals.less_1_2
25instantiation147, 52, 152  ⊢  
  : , : , :
26instantiation29, 47, 30, 31, 49, , ,  ⊢  
  : , : , :
27theorem  ⊢  
 proveit.numbers.divisibility.GCD_one_def
28instantiation32, 77  ⊢  
  : , :
29theorem  ⊢  
 proveit.numbers.divisibility.common_factor_elimination
30instantiation147, 142, 33  ⊢  
  : , : , :
31instantiation84, 34, 35, , ,  ⊢  
  : , : , :
32theorem  ⊢  
 proveit.logic.booleans.conjunction.right_from_and
33instantiation150, 151, 53  ⊢  
  : , : , :
34instantiation36, 37, 45, , ,  ⊢  
  : , : , :
35instantiation38, 47  ⊢  
  :
36theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
37instantiation39, 73, 42, 149, 40, , ,  ⊢  
  : , : , :
38theorem  ⊢  
 proveit.numbers.exponentiation.square_expansion
39theorem  ⊢  
 proveit.numbers.divisibility.common_exponent_introduction
40instantiation41, 42, 73, 43, , ,  ⊢  
  : , :
41theorem  ⊢  
 proveit.numbers.divisibility.even__if__power_is_even
42instantiation147, 52, 129  ⊢  
  : , : , :
43instantiation84, 44, 45, , ,  ⊢  
  : , : , :
44instantiation46, 47, 48, 49  ⊢  
  : , :
45instantiation84, 50, 51, , ,  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.divisibility.left_factor_divisibility
47instantiation147, 142, 55  ⊢  
  : , : , :
48instantiation147, 52, 53  ⊢  
  : , : , :
49instantiation83, 149  ⊢  
  :
50instantiation54, 55, 56, 120, 57, , ,  ⊢  
  : , : , :
51instantiation58, 59, 136, 149, 60*,  ⊢  
  : , : , :
52theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
53instantiation61, 62, 94  ⊢  
  : , :
54theorem  ⊢  
 proveit.numbers.exponentiation.exp_eq_real
55instantiation147, 130, 63  ⊢  
  : , : , :
56instantiation64, 69, 143,  ⊢  
  : , :
57instantiation65, 143, 69, 66, 67, 68*, , ,  ⊢  
  : , : , :
58theorem  ⊢  
 proveit.numbers.exponentiation.posnat_power_of_product
59instantiation147, 142, 69  ⊢  
  : , : , :
60instantiation70, 112, 71*  ⊢  
  :
61theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
62instantiation147, 72, 152  ⊢  
  : , : , :
63instantiation147, 137, 73  ⊢  
  : , : , :
64theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
65theorem  ⊢  
 proveit.numbers.multiplication.right_mult_eq_real
66instantiation74, 120, 143, 75,  ⊢  
  : , :
67instantiation76, 77  ⊢  
  : , :
68instantiation84, 78, 79,  ⊢  
  : , : , :
69instantiation147, 130, 80  ⊢  
  : , : , :
70theorem  ⊢  
 proveit.numbers.exponentiation.square_abs_rational_simp
71instantiation81, 149, 82  ⊢  
  : , :
72theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
73instantiation147, 144, 94  ⊢  
  : , : , :
74theorem  ⊢  
 proveit.numbers.division.div_real_closure
75instantiation83, 152  ⊢  
  :
76theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
77assumption  ⊢  
78instantiation84, 85, 86,  ⊢  
  : , : , :
79instantiation87, 88, 89, 90  ⊢  
  : , : , : , :
80instantiation147, 91, 92  ⊢  
  : , : , :
81theorem  ⊢  
 proveit.numbers.exponentiation.nth_power_of_nth_root
82instantiation93, 94  ⊢  
  :
83theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
84theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
85instantiation95, 109, 110, 96, 97,  ⊢  
  : , : , : , : , :
86instantiation117, 98, 99  ⊢  
  : , : , :
87theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
88instantiation126, 100  ⊢  
  : , : , :
89instantiation126, 101  ⊢  
  : , : , :
90instantiation135, 109  ⊢  
  :
91theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
92instantiation102, 103  ⊢  
  :
93theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
94theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
95theorem  ⊢  
 proveit.numbers.division.mult_frac_cancel_denom_left
96instantiation147, 105, 104  ⊢  
  : , : , :
97instantiation147, 105, 106  ⊢  
  : , : , :
98instantiation126, 107  ⊢  
  : , : , :
99instantiation126, 108  ⊢  
  : , : , :
100instantiation128, 109  ⊢  
  :
101instantiation128, 110  ⊢  
  :
102theorem  ⊢  
 proveit.numbers.absolute_value.abs_rational_nonzero_closure
103instantiation111, 112, 113  ⊢  
  :
104instantiation147, 114, 133  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
106instantiation147, 114, 115  ⊢  
  : , : , :
107instantiation126, 116  ⊢  
  : , : , :
108instantiation117, 118, 119  ⊢  
  : , : , :
109instantiation147, 142, 120  ⊢  
  : , : , :
110instantiation147, 142, 121  ⊢  
  : , : , :
111theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
112assumption  ⊢  
113instantiation122, 134, 123  ⊢  
  : , :
114theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
115instantiation147, 140, 124  ⊢  
  : , : , :
116instantiation125, 136  ⊢  
  :
117axiom  ⊢  
 proveit.logic.equality.equals_transitivity
118instantiation126, 127  ⊢  
  : , : , :
119instantiation128, 136  ⊢  
  :
120instantiation150, 151, 129  ⊢  
  : , : , :
121instantiation147, 130, 131  ⊢  
  : , : , :
122theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
123instantiation132, 133, 134  ⊢  
  : , :
124instantiation147, 148, 152  ⊢  
  : , : , :
125theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
126axiom  ⊢  
 proveit.logic.equality.substitution
127instantiation135, 136  ⊢  
  :
128theorem  ⊢  
 proveit.numbers.division.frac_one_denom
129assumption  ⊢  
130theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
131instantiation147, 137, 138  ⊢  
  : , : , :
132theorem  ⊢  
 proveit.numbers.division.div_rational_nonzero_closure
133instantiation147, 140, 139  ⊢  
  : , : , :
134instantiation147, 140, 141  ⊢  
  : , : , :
135theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
136instantiation147, 142, 143  ⊢  
  : , : , :
137theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
138instantiation147, 144, 145  ⊢  
  : , : , :
139instantiation147, 148, 146  ⊢  
  : , : , :
140theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
141instantiation147, 148, 149  ⊢  
  : , : , :
142theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
143instantiation150, 151, 152  ⊢  
  : , : , :
144theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
145theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
146theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
147theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
148theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
149theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
150theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
151instantiation153, 154  ⊢  
  : , :
152assumption  ⊢  
153theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
154theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements