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, , ,  ⊢  
  : , : , :
1theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
2instantiation4, 38, 7, 114, 5, , ,  ⊢  
  : , : , :
3reference10, , ,  ⊢  
4theorem  ⊢  
 proveit.numbers.divisibility.common_exponent_introduction
5instantiation6, 7, 38, 8, , ,  ⊢  
  : , :
6theorem  ⊢  
 proveit.numbers.divisibility.even__if__power_is_even
7instantiation112, 17, 94  ⊢  
  : , : , :
8instantiation49, 9, 10, , ,  ⊢  
  : , : , :
9instantiation11, 12, 13, 14  ⊢  
  : , :
10instantiation49, 15, 16, , ,  ⊢  
  : , : , :
11theorem  ⊢  
 proveit.numbers.divisibility.left_factor_divisibility
12instantiation112, 107, 20  ⊢  
  : , : , :
13instantiation112, 17, 18  ⊢  
  : , : , :
14instantiation48, 114  ⊢  
  :
15instantiation19, 20, 21, 85, 22, , ,  ⊢  
  : , : , :
16instantiation23, 24, 101, 114, 25*,  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
18instantiation26, 27, 59  ⊢  
  : , :
19theorem  ⊢  
 proveit.numbers.exponentiation.exp_eq_real
20instantiation112, 95, 28  ⊢  
  : , : , :
21instantiation29, 34, 108,  ⊢  
  : , :
22instantiation30, 108, 34, 31, 32, 33*, , ,  ⊢  
  : , : , :
23theorem  ⊢  
 proveit.numbers.exponentiation.posnat_power_of_product
24instantiation112, 107, 34  ⊢  
  : , : , :
25instantiation35, 77, 36*  ⊢  
  :
26theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
27instantiation112, 37, 117  ⊢  
  : , : , :
28instantiation112, 102, 38  ⊢  
  : , : , :
29theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
30theorem  ⊢  
 proveit.numbers.multiplication.right_mult_eq_real
31instantiation39, 85, 108, 40,  ⊢  
  : , :
32instantiation41, 42  ⊢  
  : , :
33instantiation49, 43, 44,  ⊢  
  : , : , :
34instantiation112, 95, 45  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.numbers.exponentiation.square_abs_rational_simp
36instantiation46, 114, 47  ⊢  
  : , :
37theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
38instantiation112, 109, 59  ⊢  
  : , : , :
39theorem  ⊢  
 proveit.numbers.division.div_real_closure
40instantiation48, 117  ⊢  
  :
41theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
42assumption  ⊢  
43instantiation49, 50, 51,  ⊢  
  : , : , :
44instantiation52, 53, 54, 55  ⊢  
  : , : , : , :
45instantiation112, 56, 57  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.exponentiation.nth_power_of_nth_root
47instantiation58, 59  ⊢  
  :
48theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
49theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
50instantiation60, 74, 75, 61, 62,  ⊢  
  : , : , : , : , :
51instantiation82, 63, 64  ⊢  
  : , : , :
52theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
53instantiation91, 65  ⊢  
  : , : , :
54instantiation91, 66  ⊢  
  : , : , :
55instantiation100, 74  ⊢  
  :
56theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
57instantiation67, 68  ⊢  
  :
58theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
59theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
60theorem  ⊢  
 proveit.numbers.division.mult_frac_cancel_denom_left
61instantiation112, 70, 69  ⊢  
  : , : , :
62instantiation112, 70, 71  ⊢  
  : , : , :
63instantiation91, 72  ⊢  
  : , : , :
64instantiation91, 73  ⊢  
  : , : , :
65instantiation93, 74  ⊢  
  :
66instantiation93, 75  ⊢  
  :
67theorem  ⊢  
 proveit.numbers.absolute_value.abs_rational_nonzero_closure
68instantiation76, 77, 78  ⊢  
  :
69instantiation112, 79, 98  ⊢  
  : , : , :
70theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
71instantiation112, 79, 80  ⊢  
  : , : , :
72instantiation91, 81  ⊢  
  : , : , :
73instantiation82, 83, 84  ⊢  
  : , : , :
74instantiation112, 107, 85  ⊢  
  : , : , :
75instantiation112, 107, 86  ⊢  
  : , : , :
76theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
77assumption  ⊢  
78instantiation87, 99, 88  ⊢  
  : , :
79theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
80instantiation112, 105, 89  ⊢  
  : , : , :
81instantiation90, 101  ⊢  
  :
82axiom  ⊢  
 proveit.logic.equality.equals_transitivity
83instantiation91, 92  ⊢  
  : , : , :
84instantiation93, 101  ⊢  
  :
85instantiation115, 116, 94  ⊢  
  : , : , :
86instantiation112, 95, 96  ⊢  
  : , : , :
87theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
88instantiation97, 98, 99  ⊢  
  : , :
89instantiation112, 113, 117  ⊢  
  : , : , :
90theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
91axiom  ⊢  
 proveit.logic.equality.substitution
92instantiation100, 101  ⊢  
  :
93theorem  ⊢  
 proveit.numbers.division.frac_one_denom
94assumption  ⊢  
95theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
96instantiation112, 102, 103  ⊢  
  : , : , :
97theorem  ⊢  
 proveit.numbers.division.div_rational_nonzero_closure
98instantiation112, 105, 104  ⊢  
  : , : , :
99instantiation112, 105, 106  ⊢  
  : , : , :
100theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
101instantiation112, 107, 108  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
103instantiation112, 109, 110  ⊢  
  : , : , :
104instantiation112, 113, 111  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
106instantiation112, 113, 114  ⊢  
  : , : , :
107theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
108instantiation115, 116, 117  ⊢  
  : , : , :
109theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
110theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
111theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
112theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
113theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
114theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
115theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
116instantiation118, 119  ⊢  
  : , :
117assumption  ⊢  
118theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
119theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements