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
0modus ponens1, 2  ⊢  
1instantiation3  ⊢  
  : , : , :
2generalization4  ⊢  
3theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
4instantiation5, 6, 7, 8,  ⊢  
  : , :
5theorem  ⊢  
 proveit.numbers.division.div_real_closure
6instantiation61, 15, 9  ⊢  
  : , : , :
7instantiation10, 11, 63,  ⊢  
  : , :
8instantiation12, 13, 14,  ⊢  
  : , :
9instantiation61, 20, 50  ⊢  
  : , : , :
10theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
11instantiation61, 15, 16,  ⊢  
  : , : , :
12theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
13instantiation61, 18, 17,  ⊢  
  : , : , :
14instantiation61, 18, 19  ⊢  
  : , : , :
15theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
16instantiation61, 20, 24,  ⊢  
  : , : , :
17instantiation61, 22, 21,  ⊢  
  : , : , :
18theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
19instantiation61, 22, 23  ⊢  
  : , : , :
20theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
21instantiation37, 24, 25,  ⊢  
  :
22theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
23theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
24instantiation61, 26, 33,  ⊢  
  : , : , :
25instantiation43, 27, 28,  ⊢  
  : , : , :
26instantiation48, 31, 32  ⊢  
  : , :
27instantiation29, 30  ⊢  
  :
28instantiation49, 31, 32, 33,  ⊢  
  : , : , :
29theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
30instantiation34, 35, 47  ⊢  
  : , :
31instantiation54, 38, 50  ⊢  
  : , :
32instantiation54, 55, 36  ⊢  
  : , :
33assumption  ⊢  
34theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
35instantiation37, 38, 39  ⊢  
  :
36instantiation61, 40, 41  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
38instantiation61, 42, 52  ⊢  
  : , : , :
39instantiation43, 44, 45  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
41instantiation46, 47  ⊢  
  :
42instantiation48, 50, 51  ⊢  
  : , :
43theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
44theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
45instantiation49, 50, 51, 52  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
47theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
48theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
49theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
50instantiation61, 62, 53  ⊢  
  : , : , :
51instantiation54, 55, 56  ⊢  
  : , :
52assumption  ⊢  
53theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
54theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
55instantiation61, 57, 58  ⊢  
  : , : , :
56instantiation59, 60  ⊢  
  :
57theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
58theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
59theorem  ⊢  
 proveit.numbers.negation.int_closure
60instantiation61, 62, 63  ⊢  
  : , : , :
61theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
62theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
63theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2