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,  ⊢  
  : , : , :
1reference67  ⊢  
2theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
3instantiation4, 9, 5,  ⊢  
  :
4theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
5instantiation6, 7,  ⊢  
  : , :
6theorem  ⊢  
 proveit.logic.equality.not_equals_symmetry
7instantiation8, 30, 9, 10,  ⊢  
  : , :
8theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
9instantiation11, 12, 13,  ⊢  
  : , :
10instantiation14, 15,  ⊢  
  : , :
11theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
12instantiation67, 55, 16,  ⊢  
  : , : , :
13instantiation17, 18  ⊢  
  :
14theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
15instantiation19, 20, 21,  ⊢  
  : , : , :
16instantiation67, 60, 22,  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.numbers.negation.real_closure
18instantiation23, 30, 52, 25  ⊢  
  : , : , :
19axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
20instantiation24, 30, 52, 25  ⊢  
  : , : , :
21instantiation37, 26, 27,  ⊢  
  : , : , :
22instantiation67, 28, 34,  ⊢  
  : , : , :
23theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
24theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
25theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
26instantiation29, 52, 30, 31, 32, 33*  ⊢  
  : , : , :
27instantiation44, 35, 58, 34,  ⊢  
  : , : , :
28instantiation53, 35, 58  ⊢  
  : , :
29theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
30theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
31instantiation67, 55, 36  ⊢  
  : , : , :
32instantiation37, 38, 39  ⊢  
  : , : , :
33instantiation40, 41, 42  ⊢  
  : , : , :
34assumption  ⊢  
35instantiation57, 43, 61  ⊢  
  : , :
36instantiation67, 60, 43  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
38theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
39instantiation44, 61, 54, 50  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
41instantiation45, 47  ⊢  
  :
42instantiation46, 47, 48  ⊢  
  : , :
43instantiation67, 49, 50  ⊢  
  : , : , :
44theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
45theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
46theorem  ⊢  
 proveit.numbers.addition.commutation
47instantiation67, 51, 52  ⊢  
  : , : , :
48theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
49instantiation53, 61, 54  ⊢  
  : , :
50assumption  ⊢  
51theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
52instantiation67, 55, 56  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
54instantiation57, 58, 59  ⊢  
  : , :
55theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
56instantiation67, 60, 61  ⊢  
  : , : , :
57theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
58instantiation67, 62, 63  ⊢  
  : , : , :
59instantiation64, 65  ⊢  
  :
60theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
61instantiation67, 68, 66  ⊢  
  : , : , :
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
65instantiation67, 68, 69  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
67theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
68theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
69theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements