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, 5  ⊢  
  : , : , :
1theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
2modus ponens6, 7  ⊢  
3modus ponens8, 9  ⊢  
4modus ponens10, 11  ⊢  
5modus ponens12, 13  ⊢  
6instantiation16  ⊢  
  : , : , :
7generalization14  ⊢  
8instantiation16  ⊢  
  : , : , :
9generalization15  ⊢  
10instantiation16  ⊢  
  : , : , :
11generalization17  ⊢  
12instantiation18  ⊢  
  : , : , :
13generalization19  ⊢  
14instantiation24, 163, 20, 21,  ⊢  
  : , :
15instantiation24, 163, 22, 23,  ⊢  
  : , :
16theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
17instantiation24, 163, 25, 26,  ⊢  
  : , :
18theorem  ⊢  
 proveit.numbers.summation.weak_summation_from_summands_bound
19instantiation27, 28, 43, 41, 29,  ⊢  
  : , : , :
20instantiation32, 68, 186,  ⊢  
  : , :
21instantiation33, 30,  ⊢  
  :
22instantiation32, 57, 186,  ⊢  
  : , :
23instantiation33, 31,  ⊢  
  :
24theorem  ⊢  
 proveit.numbers.division.div_real_closure
25instantiation32, 78, 186,  ⊢  
  : , :
26instantiation33, 34,  ⊢  
  :
27theorem  ⊢  
 proveit.numbers.division.weak_div_from_denom_bound__all_pos
28instantiation184, 35, 36  ⊢  
  : , : , :
29instantiation37, 134, 57, 78, 38, 39,  ⊢  
  : , : , :
30instantiation184, 42, 40,  ⊢  
  : , : , :
31instantiation184, 42, 41,  ⊢  
  : , : , :
32theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
33theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
34instantiation184, 42, 43,  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
36instantiation184, 44, 179  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.exponentiation.exp_even_neg_base_lesseq
38instantiation45, 46, 84,  ⊢  
  : , :
39instantiation47  ⊢  
  :
40instantiation50, 68, 48,  ⊢  
  :
41instantiation50, 57, 49,  ⊢  
  :
42theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
43instantiation50, 78, 51,  ⊢  
  :
44theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
45theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
46instantiation52, 78, 81, 128, 53, 54*,  ⊢  
  : , : , :
47axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
48instantiation55, 56,  ⊢  
  : , :
49instantiation67, 57, 128, 58,  ⊢  
  : , :
50theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
51instantiation59, 109, 60, 84,  ⊢  
  : , :
52theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
53instantiation61, 62, 128, 94, 85, 63, 64*, 65*  ⊢  
  : , : , :
54instantiation153, 66,  ⊢  
  :
55theorem  ⊢  
 proveit.logic.equality.not_equals_symmetry
56instantiation67, 128, 68, 69,  ⊢  
  : , :
57instantiation79, 78, 81,  ⊢  
  : , :
58instantiation70, 71,  ⊢  
  : , :
59theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
60theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
61theorem  ⊢  
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
62instantiation93, 163  ⊢  
  :
63instantiation72, 73  ⊢  
  : , :
64instantiation74, 75, 76  ⊢  
  : , : , :
65instantiation77, 88  ⊢  
  :
66instantiation184, 162, 78,  ⊢  
  : , : , :
67theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
68instantiation79, 80, 81,  ⊢  
  : , :
69instantiation82, 83,  ⊢  
  : , :
70theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
71instantiation164, 84, 85,  ⊢  
  : , : , :
72theorem  ⊢  
 proveit.numbers.ordering.relax_less
73instantiation117, 86  ⊢  
  :
74axiom  ⊢  
 proveit.logic.equality.equals_transitivity
75instantiation87, 179, 186, 104, 106, 105, 88, 107, 108  ⊢  
  : , : , : , : , : , :
76instantiation89, 104, 186, 105, 106, 155, 107, 108, 90*  ⊢  
  : , : , : , : , :
77theorem  ⊢  
 proveit.numbers.multiplication.mult_zero_right
78instantiation184, 168, 91,  ⊢  
  : , : , :
79theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
80instantiation184, 168, 92,  ⊢  
  : , : , :
81instantiation93, 94  ⊢  
  :
82theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
83instantiation95, 96, 97,  ⊢  
  : , : , :
84instantiation98, 99, 100,  ⊢  
  : , : , :
85instantiation101, 128, 163, 113  ⊢  
  : , : , :
86instantiation132, 146  ⊢  
  :
87theorem  ⊢  
 proveit.numbers.multiplication.disassociation
88instantiation102, 155  ⊢  
  :
89theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_any
90instantiation103, 104, 186, 105, 106, 107, 108  ⊢  
  : , : , : , :
91instantiation184, 174, 109,  ⊢  
  : , : , :
92instantiation184, 174, 110,  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.numbers.negation.real_closure
94instantiation111, 128, 163, 113  ⊢  
  : , : , :
95axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
96instantiation112, 128, 163, 113  ⊢  
  : , : , :
97instantiation164, 114, 115,  ⊢  
  : , : , :
98theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
99instantiation116, 138, 139, 125,  ⊢  
  : , : , :
100instantiation117, 118  ⊢  
  :
101theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
102theorem  ⊢  
 proveit.numbers.negation.complex_closure
103theorem  ⊢  
 proveit.numbers.multiplication.elim_one_any
104axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
105theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
106instantiation119  ⊢  
  : , :
107instantiation120, 121, 122  ⊢  
  : , :
108instantiation184, 162, 123  ⊢  
  : , : , :
109instantiation184, 124, 125,  ⊢  
  : , : , :
110instantiation184, 126, 131,  ⊢  
  : , : , :
111theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
112theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
113theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
114instantiation127, 163, 128, 129, 158, 130*  ⊢  
  : , : , :
115instantiation170, 152, 177, 131,  ⊢  
  : , : , :
116theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
117theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
118instantiation132, 133  ⊢  
  :
119theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
120theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
121instantiation184, 162, 134  ⊢  
  : , : , :
122instantiation184, 162, 135  ⊢  
  : , : , :
123instantiation136, 137  ⊢  
  :
124instantiation172, 138, 139  ⊢  
  : , :
125assumption  ⊢  
126instantiation172, 152, 177  ⊢  
  : , :
127theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
128theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
129instantiation184, 168, 140  ⊢  
  : , : , :
130instantiation141, 142, 143  ⊢  
  : , : , :
131assumption  ⊢  
132theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
133instantiation144, 145, 146  ⊢  
  : , :
134instantiation184, 168, 147  ⊢  
  : , : , :
135instantiation148, 149, 150  ⊢  
  : , : , :
136theorem  ⊢  
 proveit.physics.quantum.QPE._delta_b_is_real
137theorem  ⊢  
 proveit.physics.quantum.QPE._best_floor_is_int
138instantiation176, 151, 175  ⊢  
  : , :
139instantiation182, 152  ⊢  
  :
140instantiation184, 174, 161  ⊢  
  : , : , :
141theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
142instantiation153, 155  ⊢  
  :
143instantiation154, 155, 156  ⊢  
  : , :
144theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
145instantiation157, 161, 158  ⊢  
  :
146theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
147instantiation184, 174, 183  ⊢  
  : , : , :
148theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
149instantiation159, 160  ⊢  
  : , :
150axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
151instantiation182, 177  ⊢  
  :
152instantiation176, 161, 175  ⊢  
  : , :
153theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
154theorem  ⊢  
 proveit.numbers.addition.commutation
155instantiation184, 162, 163  ⊢  
  : , : , :
156theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
157theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
158instantiation164, 165, 166  ⊢  
  : , : , :
159theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
160theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
161instantiation184, 167, 171  ⊢  
  : , : , :
162theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
163instantiation184, 168, 169  ⊢  
  : , : , :
164theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
165theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
166instantiation170, 175, 173, 171  ⊢  
  : , : , :
167instantiation172, 175, 173  ⊢  
  : , :
168theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
169instantiation184, 174, 175  ⊢  
  : , : , :
170theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
171assumption  ⊢  
172theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
173instantiation176, 177, 178  ⊢  
  : , :
174theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
175instantiation184, 185, 179  ⊢  
  : , : , :
176theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
177instantiation184, 180, 181  ⊢  
  : , : , :
178instantiation182, 183  ⊢  
  :
179theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
180theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
181theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
182theorem  ⊢  
 proveit.numbers.negation.int_closure
183instantiation184, 185, 186  ⊢  
  : , : , :
184theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
185theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
186theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements