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.numbers.divisibility.even__if__power_is_even
2instantiation108, 13, 90  ⊢  
  : , : , :
3reference34  ⊢  
4instantiation45, 5, 6, , ,  ⊢  
  : , : , :
5instantiation7, 8, 9, 10  ⊢  
  : , :
6instantiation45, 11, 12, , ,  ⊢  
  : , : , :
7theorem  ⊢  
 proveit.numbers.divisibility.left_factor_divisibility
8instantiation108, 103, 16  ⊢  
  : , : , :
9instantiation108, 13, 14  ⊢  
  : , : , :
10instantiation44, 110  ⊢  
  :
11instantiation15, 16, 17, 81, 18, , ,  ⊢  
  : , : , :
12instantiation19, 20, 97, 110, 21*,  ⊢  
  : , : , :
13theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
14instantiation22, 23, 55  ⊢  
  : , :
15theorem  ⊢  
 proveit.numbers.exponentiation.exp_eq_real
16instantiation108, 91, 24  ⊢  
  : , : , :
17instantiation25, 30, 104,  ⊢  
  : , :
18instantiation26, 104, 30, 27, 28, 29*, , ,  ⊢  
  : , : , :
19theorem  ⊢  
 proveit.numbers.exponentiation.posnat_power_of_product
20instantiation108, 103, 30  ⊢  
  : , : , :
21instantiation31, 73, 32*  ⊢  
  :
22theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
23instantiation108, 33, 113  ⊢  
  : , : , :
24instantiation108, 98, 34  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
26theorem  ⊢  
 proveit.numbers.multiplication.right_mult_eq_real
27instantiation35, 81, 104, 36,  ⊢  
  : , :
28instantiation37, 38  ⊢  
  : , :
29instantiation45, 39, 40,  ⊢  
  : , : , :
30instantiation108, 91, 41  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.numbers.exponentiation.square_abs_rational_simp
32instantiation42, 110, 43  ⊢  
  : , :
33theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
34instantiation108, 105, 55  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.numbers.division.div_real_closure
36instantiation44, 113  ⊢  
  :
37theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
38assumption  ⊢  
39instantiation45, 46, 47,  ⊢  
  : , : , :
40instantiation48, 49, 50, 51  ⊢  
  : , : , : , :
41instantiation108, 52, 53  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.numbers.exponentiation.nth_power_of_nth_root
43instantiation54, 55  ⊢  
  :
44theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
45theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
46instantiation56, 70, 71, 57, 58,  ⊢  
  : , : , : , : , :
47instantiation78, 59, 60  ⊢  
  : , : , :
48theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
49instantiation87, 61  ⊢  
  : , : , :
50instantiation87, 62  ⊢  
  : , : , :
51instantiation96, 70  ⊢  
  :
52theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
53instantiation63, 64  ⊢  
  :
54theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
55theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
56theorem  ⊢  
 proveit.numbers.division.mult_frac_cancel_denom_left
57instantiation108, 66, 65  ⊢  
  : , : , :
58instantiation108, 66, 67  ⊢  
  : , : , :
59instantiation87, 68  ⊢  
  : , : , :
60instantiation87, 69  ⊢  
  : , : , :
61instantiation89, 70  ⊢  
  :
62instantiation89, 71  ⊢  
  :
63theorem  ⊢  
 proveit.numbers.absolute_value.abs_rational_nonzero_closure
64instantiation72, 73, 74  ⊢  
  :
65instantiation108, 75, 94  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
67instantiation108, 75, 76  ⊢  
  : , : , :
68instantiation87, 77  ⊢  
  : , : , :
69instantiation78, 79, 80  ⊢  
  : , : , :
70instantiation108, 103, 81  ⊢  
  : , : , :
71instantiation108, 103, 82  ⊢  
  : , : , :
72theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
73assumption  ⊢  
74instantiation83, 95, 84  ⊢  
  : , :
75theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
76instantiation108, 101, 85  ⊢  
  : , : , :
77instantiation86, 97  ⊢  
  :
78axiom  ⊢  
 proveit.logic.equality.equals_transitivity
79instantiation87, 88  ⊢  
  : , : , :
80instantiation89, 97  ⊢  
  :
81instantiation111, 112, 90  ⊢  
  : , : , :
82instantiation108, 91, 92  ⊢  
  : , : , :
83theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
84instantiation93, 94, 95  ⊢  
  : , :
85instantiation108, 109, 113  ⊢  
  : , : , :
86theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
87axiom  ⊢  
 proveit.logic.equality.substitution
88instantiation96, 97  ⊢  
  :
89theorem  ⊢  
 proveit.numbers.division.frac_one_denom
90assumption  ⊢  
91theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
92instantiation108, 98, 99  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.numbers.division.div_rational_nonzero_closure
94instantiation108, 101, 100  ⊢  
  : , : , :
95instantiation108, 101, 102  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
97instantiation108, 103, 104  ⊢  
  : , : , :
98theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
99instantiation108, 105, 106  ⊢  
  : , : , :
100instantiation108, 109, 107  ⊢  
  : , : , :
101theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
102instantiation108, 109, 110  ⊢  
  : , : , :
103theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
104instantiation111, 112, 113  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
106theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
107theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
108theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
109theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
110theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
111theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
112instantiation114, 115  ⊢  
  : , :
113assumption  ⊢  
114theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
115theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements