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
0generalization1  ⊢  
1deduction2, ,  ⊢  
2instantiation3, 4, 5, , ,  ⊢  
  :
3theorem  ⊢  
 proveit.logic.booleans.negation.negation_contradiction
4instantiation6, 25, 7, , ,  ⊢  
  : , :
5instantiation8, 134, 9, ,  ⊢  
  :
6theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
7instantiation26, 10, 58, 11, , ,  ⊢  
  : , :
8instantiation12, 114, 137, 13, ,  ⊢  
  : , :
9theorem  ⊢  
 proveit.numbers.numerals.decimals.less_1_2
10instantiation132, 37, 137  ⊢  
  : , : , :
11instantiation14, 32, 15, 16, 34, , ,  ⊢  
  : , : , :
12theorem  ⊢  
 proveit.numbers.divisibility.GCD_one_def
13instantiation17, 62  ⊢  
  : , :
14theorem  ⊢  
 proveit.numbers.divisibility.common_factor_elimination
15instantiation132, 127, 18  ⊢  
  : , : , :
16instantiation69, 19, 20, , ,  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.logic.booleans.conjunction.right_from_and
18instantiation135, 136, 38  ⊢  
  : , : , :
19instantiation21, 22, 30, , ,  ⊢  
  : , : , :
20instantiation23, 32  ⊢  
  :
21theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
22instantiation24, 58, 27, 134, 25, , ,  ⊢  
  : , : , :
23theorem  ⊢  
 proveit.numbers.exponentiation.square_expansion
24theorem  ⊢  
 proveit.numbers.divisibility.common_exponent_introduction
25instantiation26, 27, 58, 28, , ,  ⊢  
  : , :
26theorem  ⊢  
 proveit.numbers.divisibility.even__if__power_is_even
27instantiation132, 37, 114  ⊢  
  : , : , :
28instantiation69, 29, 30, , ,  ⊢  
  : , : , :
29instantiation31, 32, 33, 34  ⊢  
  : , :
30instantiation69, 35, 36, , ,  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.numbers.divisibility.left_factor_divisibility
32instantiation132, 127, 40  ⊢  
  : , : , :
33instantiation132, 37, 38  ⊢  
  : , : , :
34instantiation68, 134  ⊢  
  :
35instantiation39, 40, 41, 105, 42, , ,  ⊢  
  : , : , :
36instantiation43, 44, 121, 134, 45*,  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
38instantiation46, 47, 79  ⊢  
  : , :
39theorem  ⊢  
 proveit.numbers.exponentiation.exp_eq_real
40instantiation132, 115, 48  ⊢  
  : , : , :
41instantiation49, 54, 128,  ⊢  
  : , :
42instantiation50, 128, 54, 51, 52, 53*, , ,  ⊢  
  : , : , :
43theorem  ⊢  
 proveit.numbers.exponentiation.posnat_power_of_product
44instantiation132, 127, 54  ⊢  
  : , : , :
45instantiation55, 97, 56*  ⊢  
  :
46theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
47instantiation132, 57, 137  ⊢  
  : , : , :
48instantiation132, 122, 58  ⊢  
  : , : , :
49theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
50theorem  ⊢  
 proveit.numbers.multiplication.right_mult_eq_real
51instantiation59, 105, 128, 60,  ⊢  
  : , :
52instantiation61, 62  ⊢  
  : , :
53instantiation69, 63, 64,  ⊢  
  : , : , :
54instantiation132, 115, 65  ⊢  
  : , : , :
55theorem  ⊢  
 proveit.numbers.exponentiation.square_abs_rational_simp
56instantiation66, 134, 67  ⊢  
  : , :
57theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
58instantiation132, 129, 79  ⊢  
  : , : , :
59theorem  ⊢  
 proveit.numbers.division.div_real_closure
60instantiation68, 137  ⊢  
  :
61theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
62assumption  ⊢  
63instantiation69, 70, 71,  ⊢  
  : , : , :
64instantiation72, 73, 74, 75  ⊢  
  : , : , : , :
65instantiation132, 76, 77  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.numbers.exponentiation.nth_power_of_nth_root
67instantiation78, 79  ⊢  
  :
68theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
69theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
70instantiation80, 94, 95, 81, 82,  ⊢  
  : , : , : , : , :
71instantiation102, 83, 84  ⊢  
  : , : , :
72theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
73instantiation111, 85  ⊢  
  : , : , :
74instantiation111, 86  ⊢  
  : , : , :
75instantiation120, 94  ⊢  
  :
76theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
77instantiation87, 88  ⊢  
  :
78theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
79theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
80theorem  ⊢  
 proveit.numbers.division.mult_frac_cancel_denom_left
81instantiation132, 90, 89  ⊢  
  : , : , :
82instantiation132, 90, 91  ⊢  
  : , : , :
83instantiation111, 92  ⊢  
  : , : , :
84instantiation111, 93  ⊢  
  : , : , :
85instantiation113, 94  ⊢  
  :
86instantiation113, 95  ⊢  
  :
87theorem  ⊢  
 proveit.numbers.absolute_value.abs_rational_nonzero_closure
88instantiation96, 97, 98  ⊢  
  :
89instantiation132, 99, 118  ⊢  
  : , : , :
90theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
91instantiation132, 99, 100  ⊢  
  : , : , :
92instantiation111, 101  ⊢  
  : , : , :
93instantiation102, 103, 104  ⊢  
  : , : , :
94instantiation132, 127, 105  ⊢  
  : , : , :
95instantiation132, 127, 106  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
97assumption  ⊢  
98instantiation107, 119, 108  ⊢  
  : , :
99theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
100instantiation132, 125, 109  ⊢  
  : , : , :
101instantiation110, 121  ⊢  
  :
102axiom  ⊢  
 proveit.logic.equality.equals_transitivity
103instantiation111, 112  ⊢  
  : , : , :
104instantiation113, 121  ⊢  
  :
105instantiation135, 136, 114  ⊢  
  : , : , :
106instantiation132, 115, 116  ⊢  
  : , : , :
107theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
108instantiation117, 118, 119  ⊢  
  : , :
109instantiation132, 133, 137  ⊢  
  : , : , :
110theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
111axiom  ⊢  
 proveit.logic.equality.substitution
112instantiation120, 121  ⊢  
  :
113theorem  ⊢  
 proveit.numbers.division.frac_one_denom
114assumption  ⊢  
115theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
116instantiation132, 122, 123  ⊢  
  : , : , :
117theorem  ⊢  
 proveit.numbers.division.div_rational_nonzero_closure
118instantiation132, 125, 124  ⊢  
  : , : , :
119instantiation132, 125, 126  ⊢  
  : , : , :
120theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
121instantiation132, 127, 128  ⊢  
  : , : , :
122theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
123instantiation132, 129, 130  ⊢  
  : , : , :
124instantiation132, 133, 131  ⊢  
  : , : , :
125theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
126instantiation132, 133, 134  ⊢  
  : , : , :
127theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
128instantiation135, 136, 137  ⊢  
  : , : , :
129theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
130theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
131theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
132theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
133theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
134theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
135theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
136instantiation138, 139  ⊢  
  : , :
137assumption  ⊢  
138theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
139theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements