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
0deduction1  ⊢  
1modus ponens2, 3  ⊢  
2instantiation4, 5, 6, 144  ⊢  
  : , : , : , : , : , :
3instantiation16, 7, 8  ⊢  
  : , :
4theorem  ⊢  
 proveit.logic.booleans.quantification.existence.skolem_elim
5instantiation9  ⊢  
  : , :
6instantiation9  ⊢  
  : , :
7instantiation10, 87  ⊢  
  :
8generalization11  ⊢  
9theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
10theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.reduced_nat_pos_ratio
11deduction12, ,  ⊢  
12instantiation13, 14, 15, , ,  ⊢  
  :
13theorem  ⊢  
 proveit.logic.booleans.negation.negation_contradiction
14instantiation16, 35, 17, , ,  ⊢  
  : , :
15instantiation18, 144, 19, ,  ⊢  
  :
16theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
17instantiation36, 20, 68, 21, , ,  ⊢  
  : , :
18instantiation22, 124, 147, 23, ,  ⊢  
  : , :
19theorem  ⊢  
 proveit.numbers.numerals.decimals.less_1_2
20instantiation142, 47, 147  ⊢  
  : , : , :
21instantiation24, 42, 25, 26, 44, , ,  ⊢  
  : , : , :
22theorem  ⊢  
 proveit.numbers.divisibility.GCD_one_def
23instantiation27, 72  ⊢  
  : , :
24theorem  ⊢  
 proveit.numbers.divisibility.common_factor_elimination
25instantiation142, 137, 28  ⊢  
  : , : , :
26instantiation79, 29, 30, , ,  ⊢  
  : , : , :
27theorem  ⊢  
 proveit.logic.booleans.conjunction.right_from_and
28instantiation145, 146, 48  ⊢  
  : , : , :
29instantiation31, 32, 40, , ,  ⊢  
  : , : , :
30instantiation33, 42  ⊢  
  :
31theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
32instantiation34, 68, 37, 144, 35, , ,  ⊢  
  : , : , :
33theorem  ⊢  
 proveit.numbers.exponentiation.square_expansion
34theorem  ⊢  
 proveit.numbers.divisibility.common_exponent_introduction
35instantiation36, 37, 68, 38, , ,  ⊢  
  : , :
36theorem  ⊢  
 proveit.numbers.divisibility.even__if__power_is_even
37instantiation142, 47, 124  ⊢  
  : , : , :
38instantiation79, 39, 40, , ,  ⊢  
  : , : , :
39instantiation41, 42, 43, 44  ⊢  
  : , :
40instantiation79, 45, 46, , ,  ⊢  
  : , : , :
41theorem  ⊢  
 proveit.numbers.divisibility.left_factor_divisibility
42instantiation142, 137, 50  ⊢  
  : , : , :
43instantiation142, 47, 48  ⊢  
  : , : , :
44instantiation78, 144  ⊢  
  :
45instantiation49, 50, 51, 115, 52, , ,  ⊢  
  : , : , :
46instantiation53, 54, 131, 144, 55*,  ⊢  
  : , : , :
47theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
48instantiation56, 57, 89  ⊢  
  : , :
49theorem  ⊢  
 proveit.numbers.exponentiation.exp_eq_real
50instantiation142, 125, 58  ⊢  
  : , : , :
51instantiation59, 64, 138,  ⊢  
  : , :
52instantiation60, 138, 64, 61, 62, 63*, , ,  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.exponentiation.posnat_power_of_product
54instantiation142, 137, 64  ⊢  
  : , : , :
55instantiation65, 107, 66*  ⊢  
  :
56theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
57instantiation142, 67, 147  ⊢  
  : , : , :
58instantiation142, 132, 68  ⊢  
  : , : , :
59theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
60theorem  ⊢  
 proveit.numbers.multiplication.right_mult_eq_real
61instantiation69, 115, 138, 70,  ⊢  
  : , :
62instantiation71, 72  ⊢  
  : , :
63instantiation79, 73, 74,  ⊢  
  : , : , :
64instantiation142, 125, 75  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.numbers.exponentiation.square_abs_rational_simp
66instantiation76, 144, 77  ⊢  
  : , :
67theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
68instantiation142, 139, 89  ⊢  
  : , : , :
69theorem  ⊢  
 proveit.numbers.division.div_real_closure
70instantiation78, 147  ⊢  
  :
71theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
72assumption  ⊢  
73instantiation79, 80, 81,  ⊢  
  : , : , :
74instantiation82, 83, 84, 85  ⊢  
  : , : , : , :
75instantiation142, 86, 87  ⊢  
  : , : , :
76theorem  ⊢  
 proveit.numbers.exponentiation.nth_power_of_nth_root
77instantiation88, 89  ⊢  
  :
78theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
79theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
80instantiation90, 104, 105, 91, 92,  ⊢  
  : , : , : , : , :
81instantiation112, 93, 94  ⊢  
  : , : , :
82theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
83instantiation121, 95  ⊢  
  : , : , :
84instantiation121, 96  ⊢  
  : , : , :
85instantiation130, 104  ⊢  
  :
86theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
87instantiation97, 98  ⊢  
  :
88theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
89theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
90theorem  ⊢  
 proveit.numbers.division.mult_frac_cancel_denom_left
91instantiation142, 100, 99  ⊢  
  : , : , :
92instantiation142, 100, 101  ⊢  
  : , : , :
93instantiation121, 102  ⊢  
  : , : , :
94instantiation121, 103  ⊢  
  : , : , :
95instantiation123, 104  ⊢  
  :
96instantiation123, 105  ⊢  
  :
97theorem  ⊢  
 proveit.numbers.absolute_value.abs_rational_nonzero_closure
98instantiation106, 107, 108  ⊢  
  :
99instantiation142, 109, 128  ⊢  
  : , : , :
100theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
101instantiation142, 109, 110  ⊢  
  : , : , :
102instantiation121, 111  ⊢  
  : , : , :
103instantiation112, 113, 114  ⊢  
  : , : , :
104instantiation142, 137, 115  ⊢  
  : , : , :
105instantiation142, 137, 116  ⊢  
  : , : , :
106theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero
107assumption  ⊢  
108instantiation117, 129, 118  ⊢  
  : , :
109theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
110instantiation142, 135, 119  ⊢  
  : , : , :
111instantiation120, 131  ⊢  
  :
112axiom  ⊢  
 proveit.logic.equality.equals_transitivity
113instantiation121, 122  ⊢  
  : , : , :
114instantiation123, 131  ⊢  
  :
115instantiation145, 146, 124  ⊢  
  : , : , :
116instantiation142, 125, 126  ⊢  
  : , : , :
117theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
118instantiation127, 128, 129  ⊢  
  : , :
119instantiation142, 143, 147  ⊢  
  : , : , :
120theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
121axiom  ⊢  
 proveit.logic.equality.substitution
122instantiation130, 131  ⊢  
  :
123theorem  ⊢  
 proveit.numbers.division.frac_one_denom
124assumption  ⊢  
125theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
126instantiation142, 132, 133  ⊢  
  : , : , :
127theorem  ⊢  
 proveit.numbers.division.div_rational_nonzero_closure
128instantiation142, 135, 134  ⊢  
  : , : , :
129instantiation142, 135, 136  ⊢  
  : , : , :
130theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
131instantiation142, 137, 138  ⊢  
  : , : , :
132theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
133instantiation142, 139, 140  ⊢  
  : , : , :
134instantiation142, 143, 141  ⊢  
  : , : , :
135theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
136instantiation142, 143, 144  ⊢  
  : , : , :
137theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
138instantiation145, 146, 147  ⊢  
  : , : , :
139theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
140theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
141theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
142theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
143theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
144theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
145theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
146instantiation148, 149  ⊢  
  : , :
147assumption  ⊢  
148theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
149theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements