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  ⊢  
  :
1theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
2instantiation65, 3, 4  ⊢  
  : , : , :
3theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
4modus ponens5, 6  ⊢  
5instantiation7  ⊢  
  : , : , :
6generalization8  ⊢  
7theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
8instantiation9, 10, 11, 12,  ⊢  
  : , :
9theorem  ⊢  
 proveit.numbers.division.div_real_closure
10instantiation65, 19, 13  ⊢  
  : , : , :
11instantiation14, 15, 67,  ⊢  
  : , :
12instantiation16, 17, 18,  ⊢  
  : , :
13instantiation65, 24, 54  ⊢  
  : , : , :
14theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
15instantiation65, 19, 20,  ⊢  
  : , : , :
16theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
17instantiation65, 22, 21,  ⊢  
  : , : , :
18instantiation65, 22, 23  ⊢  
  : , : , :
19theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
20instantiation65, 24, 28,  ⊢  
  : , : , :
21instantiation65, 26, 25,  ⊢  
  : , : , :
22theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
23instantiation65, 26, 27  ⊢  
  : , : , :
24theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
25instantiation41, 28, 29,  ⊢  
  :
26theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
27theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
28instantiation65, 30, 37,  ⊢  
  : , : , :
29instantiation47, 31, 32,  ⊢  
  : , : , :
30instantiation52, 35, 36  ⊢  
  : , :
31instantiation33, 34  ⊢  
  :
32instantiation53, 35, 36, 37,  ⊢  
  : , : , :
33theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
34instantiation38, 39, 51  ⊢  
  : , :
35instantiation58, 42, 54  ⊢  
  : , :
36instantiation58, 59, 40  ⊢  
  : , :
37assumption  ⊢  
38theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
39instantiation41, 42, 43  ⊢  
  :
40instantiation65, 44, 45  ⊢  
  : , : , :
41theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
42instantiation65, 46, 56  ⊢  
  : , : , :
43instantiation47, 48, 49  ⊢  
  : , : , :
44theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
45instantiation50, 51  ⊢  
  :
46instantiation52, 54, 55  ⊢  
  : , :
47theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
48theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
49instantiation53, 54, 55, 56  ⊢  
  : , : , :
50theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
51theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
52theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
53theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
54instantiation65, 66, 57  ⊢  
  : , : , :
55instantiation58, 59, 60  ⊢  
  : , :
56assumption  ⊢  
57theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
58theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
59instantiation65, 61, 62  ⊢  
  : , : , :
60instantiation63, 64  ⊢  
  :
61theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
62theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
63theorem  ⊢  
 proveit.numbers.negation.int_closure
64instantiation65, 66, 67  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
66theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
67theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2