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
2reference55  ⊢  
3instantiation5, 6, 72,  ⊢  
  : , :
4instantiation7, 8,  ⊢  
  :
5theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
6instantiation9, 10, 11,  ⊢  
  : , :
7theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
8instantiation12, 13, 72,  ⊢  
  : , :
9theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
10instantiation70, 58, 14,  ⊢  
  : , : , :
11instantiation15, 55  ⊢  
  :
12theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
13instantiation16, 17, 18,  ⊢  
  :
14instantiation70, 63, 19,  ⊢  
  : , : , :
15theorem  ⊢  
 proveit.numbers.negation.real_closure
16theorem  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
17instantiation60, 19, 20,  ⊢  
  : , :
18instantiation21, 22,  ⊢  
  : , :
19instantiation70, 23, 38,  ⊢  
  : , : , :
20instantiation70, 24, 25  ⊢  
  : , : , :
21theorem  ⊢  
 proveit.numbers.ordering.relax_less
22instantiation26, 27,  ⊢  
  : , :
23instantiation56, 37, 61  ⊢  
  : , :
24theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
25instantiation28, 29  ⊢  
  :
26theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
27instantiation40, 30, 31,  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
29theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
30instantiation32, 55, 33, 34, 35, 36*  ⊢  
  : , : , :
31instantiation47, 37, 61, 38,  ⊢  
  : , : , :
32theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
33theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
34instantiation70, 58, 39  ⊢  
  : , : , :
35instantiation40, 41, 42  ⊢  
  : , : , :
36instantiation43, 44, 45  ⊢  
  : , : , :
37instantiation60, 46, 64  ⊢  
  : , :
38assumption  ⊢  
39instantiation70, 63, 46  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
41theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
42instantiation47, 64, 57, 53  ⊢  
  : , : , :
43theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
44instantiation48, 50  ⊢  
  :
45instantiation49, 50, 51  ⊢  
  : , :
46instantiation70, 52, 53  ⊢  
  : , : , :
47theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
48theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
49theorem  ⊢  
 proveit.numbers.addition.commutation
50instantiation70, 54, 55  ⊢  
  : , : , :
51theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
52instantiation56, 64, 57  ⊢  
  : , :
53assumption  ⊢  
54theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
55instantiation70, 58, 59  ⊢  
  : , : , :
56theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
57instantiation60, 61, 62  ⊢  
  : , :
58theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
59instantiation70, 63, 64  ⊢  
  : , : , :
60theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
61instantiation70, 65, 66  ⊢  
  : , : , :
62instantiation67, 68  ⊢  
  :
63theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
64instantiation70, 71, 69  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
66theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
67theorem  ⊢  
 proveit.numbers.negation.int_closure
68instantiation70, 71, 72  ⊢  
  : , : , :
69theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
70theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
71theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
72theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements