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.ordering.less_is_not_eq
2reference24  ⊢  
3instantiation5, 6, 7,  ⊢  
  : , :
4instantiation8, 9,  ⊢  
  : , :
5theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
6instantiation61, 49, 10,  ⊢  
  : , : , :
7instantiation11, 12  ⊢  
  :
8theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
9instantiation13, 14, 15,  ⊢  
  : , : , :
10instantiation61, 54, 16,  ⊢  
  : , : , :
11theorem  ⊢  
 proveit.numbers.negation.real_closure
12instantiation17, 24, 46, 19  ⊢  
  : , : , :
13axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
14instantiation18, 24, 46, 19  ⊢  
  : , : , :
15instantiation31, 20, 21,  ⊢  
  : , : , :
16instantiation61, 22, 28,  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
18theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
19theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
20instantiation23, 46, 24, 25, 26, 27*  ⊢  
  : , : , :
21instantiation38, 29, 52, 28,  ⊢  
  : , : , :
22instantiation47, 29, 52  ⊢  
  : , :
23theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
24theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
25instantiation61, 49, 30  ⊢  
  : , : , :
26instantiation31, 32, 33  ⊢  
  : , : , :
27instantiation34, 35, 36  ⊢  
  : , : , :
28assumption  ⊢  
29instantiation51, 37, 55  ⊢  
  : , :
30instantiation61, 54, 37  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
32theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
33instantiation38, 55, 48, 44  ⊢  
  : , : , :
34theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
35instantiation39, 41  ⊢  
  :
36instantiation40, 41, 42  ⊢  
  : , :
37instantiation61, 43, 44  ⊢  
  : , : , :
38theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
39theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
40theorem  ⊢  
 proveit.numbers.addition.commutation
41instantiation61, 45, 46  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
43instantiation47, 55, 48  ⊢  
  : , :
44assumption  ⊢  
45theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
46instantiation61, 49, 50  ⊢  
  : , : , :
47theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
48instantiation51, 52, 53  ⊢  
  : , :
49theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
50instantiation61, 54, 55  ⊢  
  : , : , :
51theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
52instantiation61, 56, 57  ⊢  
  : , : , :
53instantiation58, 59  ⊢  
  :
54theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
55instantiation61, 62, 60  ⊢  
  : , : , :
56theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
57theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
58theorem  ⊢  
 proveit.numbers.negation.int_closure
59instantiation61, 62, 63  ⊢  
  : , : , :
60theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
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
*equality replacement requirements