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