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,  ⊢  
  : , :
1theorem  ⊢  
 proveit.numbers.division.div_real_closure
2reference32  ⊢  
3instantiation5, 13, 73,  ⊢  
  : , :
4instantiation6, 7,  ⊢  
  :
5theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
6theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
7instantiation71, 8, 9,  ⊢  
  : , : , :
8theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
9instantiation10, 13, 11,  ⊢  
  :
10theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
11instantiation12, 13, 31, 14,  ⊢  
  : , :
12theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
13instantiation15, 16, 17,  ⊢  
  : , :
14instantiation18, 19,  ⊢  
  : , :
15theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
16instantiation71, 39, 20,  ⊢  
  : , : , :
17instantiation21, 22  ⊢  
  :
18theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
19instantiation55, 23, 24,  ⊢  
  : , : , :
20instantiation71, 45, 25,  ⊢  
  : , : , :
21theorem  ⊢  
 proveit.numbers.negation.real_closure
22instantiation26, 31, 32, 33  ⊢  
  : , : , :
23instantiation27, 28, 29,  ⊢  
  : , : , :
24instantiation30, 31, 32, 33  ⊢  
  : , : , :
25instantiation71, 34, 36,  ⊢  
  : , : , :
26theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
27theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
28instantiation35, 41, 42, 36,  ⊢  
  : , : , :
29instantiation37, 38  ⊢  
  :
30theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
31theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
32instantiation71, 39, 40  ⊢  
  : , : , :
33theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
34instantiation58, 41, 42  ⊢  
  : , :
35theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
36assumption  ⊢  
37theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
38instantiation43, 44  ⊢  
  :
39theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
40instantiation71, 45, 60  ⊢  
  : , : , :
41instantiation64, 46, 60  ⊢  
  : , :
42instantiation69, 47  ⊢  
  :
43theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
44instantiation48, 49, 50  ⊢  
  : , :
45theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
46instantiation69, 65  ⊢  
  :
47instantiation64, 52, 60  ⊢  
  : , :
48theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
49instantiation51, 52, 53  ⊢  
  :
50theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
51theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
52instantiation71, 54, 62  ⊢  
  : , : , :
53instantiation55, 56, 57  ⊢  
  : , : , :
54instantiation58, 60, 61  ⊢  
  : , :
55theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
56theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
57instantiation59, 60, 61, 62  ⊢  
  : , : , :
58theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
59theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
60instantiation71, 72, 63  ⊢  
  : , : , :
61instantiation64, 65, 66  ⊢  
  : , :
62assumption  ⊢  
63theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
64theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
65instantiation71, 67, 68  ⊢  
  : , : , :
66instantiation69, 70  ⊢  
  :
67theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
68theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
69theorem  ⊢  
 proveit.numbers.negation.int_closure
70instantiation71, 72, 73  ⊢  
  : , : , :
71theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
72theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
73theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2