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, 5, 6, 7*,  ⊢  
  : , : , : , : , :
1theorem  ⊢  
 proveit.numbers.summation.sum_split_after
2reference33  ⊢  
3instantiation57, 58, 8  ⊢  
  : , : , :
4reference52  ⊢  
5instantiation9, 10, 11,  ⊢  
  : , : , :
6theorem  ⊢  
 proveit.numbers.numerals.decimals.less_8_9
7instantiation12, 13, 14  ⊢  
  : , : , :
8theorem  ⊢  
 proveit.numbers.numerals.decimals.nat8
9theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
10instantiation15, 16, 38, 17, 18, 19,  ⊢  
  : , : , :
11theorem  ⊢  
 proveit.numbers.numerals.decimals.add_7_1
12axiom  ⊢  
 proveit.logic.equality.equals_transitivity
13instantiation53, 20  ⊢  
  : , : , :
14instantiation21, 52, 22*  ⊢  
  : , :
15theorem  ⊢  
 proveit.numbers.ordering.less_eq_add_right
16instantiation57, 46, 23  ⊢  
  : , : , :
17instantiation57, 46, 24  ⊢  
  : , : , :
18assumption  ⊢  
19instantiation25, 42  ⊢  
  :
20modus ponens26, 27  ⊢  
21axiom  ⊢  
 proveit.numbers.summation.sum_single
22instantiation28, 29, 30, 31, 32  ⊢  
  : , : , :
23instantiation57, 51, 33  ⊢  
  : , : , :
24instantiation57, 51, 34  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
26instantiation35, 36  ⊢  
  : , : , : , : , : , :
27generalization37  ⊢  
28theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
29instantiation57, 40, 38  ⊢  
  : , : , :
30instantiation57, 40, 39  ⊢  
  : , : , :
31instantiation57, 40, 41  ⊢  
  : , : , :
32theorem  ⊢  
 proveit.numbers.numerals.decimals.add_7_2
33assumption  ⊢  
34instantiation57, 58, 42  ⊢  
  : , : , :
35axiom  ⊢  
 proveit.core_expr_types.lambda_maps.lambda_substitution
36theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
37instantiation53, 43  ⊢  
  : , : , :
38instantiation57, 46, 44  ⊢  
  : , : , :
39instantiation57, 46, 45  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
41instantiation57, 46, 47  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
43instantiation53, 48  ⊢  
  : , : , :
44instantiation57, 51, 49  ⊢  
  : , : , :
45instantiation57, 51, 50  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
47instantiation57, 51, 52  ⊢  
  : , : , :
48instantiation53, 54  ⊢  
  : , : , :
49instantiation57, 58, 55  ⊢  
  : , : , :
50instantiation57, 58, 56  ⊢  
  : , : , :
51theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
52instantiation57, 58, 59  ⊢  
  : , : , :
53axiom  ⊢  
 proveit.logic.equality.substitution
54theorem  ⊢  
 proveit.numbers.numerals.decimals.add_8_1
55theorem  ⊢  
 proveit.numbers.numerals.decimals.nat7
56theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
57theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
58theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
59theorem  ⊢  
 proveit.numbers.numerals.decimals.nat9
*equality replacement requirements