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.number_sets.real_numbers.nonzero_if_in_real_nonzero
2instantiation66, 3, 4,  ⊢  
  : , : , :
3theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
4instantiation5, 8, 6,  ⊢  
  :
5theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
6instantiation7, 8, 26, 9,  ⊢  
  : , :
7theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
8instantiation10, 11, 12,  ⊢  
  : , :
9instantiation13, 14,  ⊢  
  : , :
10theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
11instantiation66, 34, 15,  ⊢  
  : , : , :
12instantiation16, 17  ⊢  
  :
13theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
14instantiation50, 18, 19,  ⊢  
  : , : , :
15instantiation66, 40, 20,  ⊢  
  : , : , :
16theorem  ⊢  
 proveit.numbers.negation.real_closure
17instantiation21, 26, 27, 28  ⊢  
  : , : , :
18instantiation22, 23, 24,  ⊢  
  : , : , :
19instantiation25, 26, 27, 28  ⊢  
  : , : , :
20instantiation66, 29, 31,  ⊢  
  : , : , :
21theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
22theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
23instantiation30, 36, 37, 31,  ⊢  
  : , : , :
24instantiation32, 33  ⊢  
  :
25theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
26theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
27instantiation66, 34, 35  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
29instantiation53, 36, 37  ⊢  
  : , :
30theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
31assumption  ⊢  
32theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
33instantiation38, 39  ⊢  
  :
34theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
35instantiation66, 40, 55  ⊢  
  : , : , :
36instantiation59, 41, 55  ⊢  
  : , :
37instantiation64, 42  ⊢  
  :
38theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
39instantiation43, 44, 45  ⊢  
  : , :
40theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
41instantiation64, 60  ⊢  
  :
42instantiation59, 47, 55  ⊢  
  : , :
43theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
44instantiation46, 47, 48  ⊢  
  :
45theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
46theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
47instantiation66, 49, 57  ⊢  
  : , : , :
48instantiation50, 51, 52  ⊢  
  : , : , :
49instantiation53, 55, 56  ⊢  
  : , :
50theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
51theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
52instantiation54, 55, 56, 57  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
54theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
55instantiation66, 67, 58  ⊢  
  : , : , :
56instantiation59, 60, 61  ⊢  
  : , :
57assumption  ⊢  
58theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
59theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
60instantiation66, 62, 63  ⊢  
  : , : , :
61instantiation64, 65  ⊢  
  :
62theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
63theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
64theorem  ⊢  
 proveit.numbers.negation.int_closure
65instantiation66, 67, 68  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
67theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
68theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2