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
0modus ponens1, 2  ⊢  
1instantiation3  ⊢  
  : , : , :
2generalization4  ⊢  
3theorem  ⊢  
 proveit.numbers.summation.weak_summation_from_summands_bound
4instantiation5, 6, 7, 8, 9,  ⊢  
  : , : , :
5theorem  ⊢  
 proveit.numbers.division.weak_div_from_denom_bound__all_pos
6instantiation128, 10, 11  ⊢  
  : , : , :
7instantiation13, 58, 12,  ⊢  
  :
8instantiation13, 22, 14,  ⊢  
  :
9instantiation15, 93, 22, 58, 16, 17,  ⊢  
  : , : , :
10theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
11instantiation128, 18, 120  ⊢  
  : , : , :
12instantiation19, 78, 20, 34,  ⊢  
  : , :
13theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
14instantiation21, 22, 50, 23,  ⊢  
  : , :
15theorem  ⊢  
 proveit.numbers.exponentiation.exp_even_neg_base_lesseq
16instantiation24, 25, 34,  ⊢  
  : , :
17instantiation26  ⊢  
  :
18theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
19theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
20theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
21theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
22instantiation27, 58, 31,  ⊢  
  : , :
23instantiation28, 29,  ⊢  
  : , :
24theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
25instantiation30, 58, 31, 50, 32, 33*,  ⊢  
  : , : , :
26axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
27theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
28theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
29instantiation100, 34, 38,  ⊢  
  : , : , :
30theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
31instantiation47, 37  ⊢  
  :
32instantiation35, 36, 50, 37, 38, 39, 40*, 41*  ⊢  
  : , : , :
33instantiation42, 43,  ⊢  
  :
34instantiation44, 45, 46,  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
36instantiation47, 82  ⊢  
  :
37instantiation48, 50, 82, 51  ⊢  
  : , : , :
38instantiation49, 50, 82, 51  ⊢  
  : , : , :
39instantiation52, 53  ⊢  
  : , :
40instantiation54, 55, 56  ⊢  
  : , : , :
41instantiation57, 64  ⊢  
  :
42theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
43instantiation128, 94, 58,  ⊢  
  : , : , :
44theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
45instantiation59, 98, 99, 89,  ⊢  
  : , : , :
46instantiation61, 60  ⊢  
  :
47theorem  ⊢  
 proveit.numbers.negation.real_closure
48theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
49theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
50theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
51theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
52theorem  ⊢  
 proveit.numbers.ordering.relax_less
53instantiation61, 62  ⊢  
  :
54axiom  ⊢  
 proveit.logic.equality.equals_transitivity
55instantiation63, 120, 130, 73, 75, 74, 64, 76, 77  ⊢  
  : , : , : , : , : , :
56instantiation65, 73, 130, 74, 75, 71, 76, 77, 66*  ⊢  
  : , : , : , : , :
57theorem  ⊢  
 proveit.numbers.multiplication.mult_zero_right
58instantiation128, 103, 67,  ⊢  
  : , : , :
59theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
60instantiation69, 68  ⊢  
  :
61theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
62instantiation69, 81  ⊢  
  :
63theorem  ⊢  
 proveit.numbers.multiplication.disassociation
64instantiation70, 71  ⊢  
  :
65theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_any
66instantiation72, 73, 130, 74, 75, 76, 77  ⊢  
  : , : , : , :
67instantiation128, 111, 78,  ⊢  
  : , : , :
68instantiation79, 80, 81  ⊢  
  : , :
69theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
70theorem  ⊢  
 proveit.numbers.negation.complex_closure
71instantiation128, 94, 82  ⊢  
  : , : , :
72theorem  ⊢  
 proveit.numbers.multiplication.elim_one_any
73axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
74theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
75instantiation83  ⊢  
  : , :
76instantiation84, 85, 86  ⊢  
  : , :
77instantiation128, 94, 87  ⊢  
  : , : , :
78instantiation128, 88, 89,  ⊢  
  : , : , :
79theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
80instantiation90, 114, 91  ⊢  
  :
81theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
82instantiation128, 103, 92  ⊢  
  : , : , :
83theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
84theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
85instantiation128, 94, 93  ⊢  
  : , : , :
86instantiation128, 94, 95  ⊢  
  : , : , :
87instantiation96, 97  ⊢  
  :
88instantiation117, 98, 99  ⊢  
  : , :
89assumption  ⊢  
90theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
91instantiation100, 101, 102  ⊢  
  : , : , :
92instantiation128, 111, 118  ⊢  
  : , : , :
93instantiation128, 103, 104  ⊢  
  : , : , :
94theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
95instantiation105, 106, 107  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.physics.quantum.QPE._delta_b_is_real
97theorem  ⊢  
 proveit.physics.quantum.QPE._best_floor_is_int
98instantiation121, 108, 118  ⊢  
  : , :
99instantiation126, 109  ⊢  
  :
100theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
101theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
102instantiation110, 118, 119, 116  ⊢  
  : , : , :
103theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
104instantiation128, 111, 127  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
106instantiation112, 113  ⊢  
  : , :
107axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
108instantiation126, 122  ⊢  
  :
109instantiation121, 114, 118  ⊢  
  : , :
110theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
111theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
112theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
113theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
114instantiation128, 115, 116  ⊢  
  : , : , :
115instantiation117, 118, 119  ⊢  
  : , :
116assumption  ⊢  
117theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
118instantiation128, 129, 120  ⊢  
  : , : , :
119instantiation121, 122, 123  ⊢  
  : , :
120theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
121theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
122instantiation128, 124, 125  ⊢  
  : , : , :
123instantiation126, 127  ⊢  
  :
124theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
125theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
126theorem  ⊢  
 proveit.numbers.negation.int_closure
127instantiation128, 129, 130  ⊢  
  : , : , :
128theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
129theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
130theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements