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
0generalization1  ⊢  
1instantiation2, 3, 4, 5,  ⊢  
  : , :
2theorem  ⊢  
 proveit.numbers.division.div_real_closure
3instantiation59, 15, 6  ⊢  
  : , : , :
4instantiation7, 13, 61,  ⊢  
  : , :
5instantiation8, 9,  ⊢  
  :
6instantiation59, 20, 48  ⊢  
  : , : , :
7theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
8theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
9instantiation59, 10, 11,  ⊢  
  : , : , :
10theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
11instantiation12, 13, 14,  ⊢  
  :
12theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
13instantiation59, 15, 16,  ⊢  
  : , : , :
14instantiation17, 21, 18, 19,  ⊢  
  : , :
15theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
16instantiation59, 20, 21,  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
18theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
19instantiation22, 23, 24,  ⊢  
  : , : , :
20theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
21instantiation59, 25, 27,  ⊢  
  : , : , :
22theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
23instantiation26, 30, 31, 27,  ⊢  
  : , : , :
24instantiation28, 29  ⊢  
  :
25instantiation46, 30, 31  ⊢  
  : , :
26theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
27assumption  ⊢  
28theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
29instantiation32, 33  ⊢  
  :
30instantiation52, 34, 48  ⊢  
  : , :
31instantiation57, 35  ⊢  
  :
32theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
33instantiation36, 37, 38  ⊢  
  : , :
34instantiation57, 53  ⊢  
  :
35instantiation52, 40, 48  ⊢  
  : , :
36theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
37instantiation39, 40, 41  ⊢  
  :
38theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
39theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
40instantiation59, 42, 50  ⊢  
  : , : , :
41instantiation43, 44, 45  ⊢  
  : , : , :
42instantiation46, 48, 49  ⊢  
  : , :
43theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
44theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
45instantiation47, 48, 49, 50  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
47theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
48instantiation59, 60, 51  ⊢  
  : , : , :
49instantiation52, 53, 54  ⊢  
  : , :
50assumption  ⊢  
51theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
52theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
53instantiation59, 55, 56  ⊢  
  : , : , :
54instantiation57, 58  ⊢  
  :
55theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
56theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
57theorem  ⊢  
 proveit.numbers.negation.int_closure
58instantiation59, 60, 61  ⊢  
  : , : , :
59theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
60theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
61theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2