import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, l, m, defaults
from proveit.logic import InSet
from proveit.numbers import Abs, Integer, Real, subtract, Mult, Exp
from proveit.physics.quantum.QPE import ModAdd
from proveit.physics.quantum.QPE import (
_alpha_are_complex, _alpha_summed,
_b_floor, _best_floor_is_int, _delta_b_floor_diff_in_interval,
_delta_b_is_real, _delta_b_not_eq_scaledNonzeroInt, _mod_add_closure,
_scaled_abs_delta_b_floor_diff_interval, _scaled_delta_b_not_eq_nonzeroInt,
_scaled_delta_b_floor_in_interval, _non_int_delta_b_diff,
_t_in_natural_pos, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos)
%proving _alpha_sqrd_upper_bound
Keep the factor of $2$ from combining with $2^t$ in the steps below:
Exp.change_simplification_directives(factor_numeric_rational=True)
_two_pow_t_minus_one_is_nat_pos
_scaled_delta_b_floor_in_interval
InSet(subtract(_scaled_delta_b_floor_in_interval.element, l), Real).prove()
_scaled_abs_delta_b_floor_diff_interval.instantiate()
_delta_b_not_eq_scaledNonzeroInt.instantiate({b: _b_floor})
_delta_b_floor_diff_in_interval.instantiate()
_scaled_delta_b_not_eq_nonzeroInt.instantiate({b: _b_floor})
_best_floor_is_int
_b_floor_plus_ell_in_interval = _mod_add_closure.instantiate({a: _b_floor, b:l})
_delta_b_is_real.instantiate({b: _b_floor})
_two_pow_t_is_nat_pos
_b_floor_plus_ell_in_interval.derive_element_in_integer()
_alpha_are_complex.instantiate({m: ModAdd(_b_floor, l)})
_alpha_summed
¶_alpha_summed_inst = _alpha_summed.instantiate()
# We want to temporarily preserve the resulting numerator
# so it isn't auto-simplified, so we first give it a convenient label
numerator = Abs(_alpha_summed_inst.rhs.factors[1].numerator)
_non_int_delta_b_diff
_non_int_delta_b_diff.instantiate({b:_b_floor})
# In applying the Abs() to both sides, we avoid the auto-simplifying
# chord-length simplification in the numerator by using 'preserve_expr':
_alpha_summed_inst_abs = _alpha_summed_inst.abs_both_sides(preserve_expr=numerator)
_alpha_summed_inst_abs_dist = (
_alpha_summed_inst_abs.inner_expr().rhs.distribute(preserve_expr=numerator))
numer_bound = numerator.deduce_triangle_bound()
denom_sin_bound = denom_sin.deduce_linear_bound()
sin_bound_is_positive = denom_sin_bound.rhs.deduce_positive()
denom_sin_is_positive = denom_sin_bound.apply_transitivity(sin_bound_is_positive)
denom_bound = denominator.deduce_bound(denom_sin_bound)
denom_is_positive = denominator.deduce_bound(denom_sin_is_positive)
# recall from earlier:
_alpha_summed_inst_abs_dist
rhs_bound = _alpha_summed_inst_abs_dist.rhs.deduce_bound([numer_bound, denom_bound])
alpha_upper_bound_01 = _alpha_summed_inst_abs_dist.apply_transitivity(rhs_bound)
alpha_upper_bound_02 = alpha_upper_bound_01.inner_expr().rhs.denominator.associate(1, 2)
alpha_upper_bound_03 = (
alpha_upper_bound_02.inner_expr().rhs.denominator.operands[1].distribute(1))
with Exp.temporary_simplification_directives() as tmp_directives:
tmp_directives.distribute_exponent=True
alpha_upper_bound_03.square_both_sides()
_alpha_sqrd_upper_bound may now be readily provable (assuming required theorems are usable). Simply execute "%qed".
%qed
proveit.physics.quantum.QPE._alpha_sqrd_upper_bound has been proven.
step type | requirements | statement | ||
---|---|---|---|---|
0 | generalization | 1 | ⊢ | |
1 | instantiation | 576, 2, 3 | ||
2 | instantiation | 4, 684, 5, 6, 7, 8, 9* | ||
3 | instantiation | 667, 10 | ||
4 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.exp_pos_lesseq | ||||
5 | instantiation | 705, 500, 21 | ||
6 | instantiation | 428, 657, 24, 16 | ||
7 | instantiation | 343, 11, 12 | ||
8 | instantiation | 13, 696 | ⊢ | |
9 | instantiation | 14, 642, 15, 696, 16, 17*, 18* | ||
10 | instantiation | 667, 19 | ||
11 | instantiation | 20, 21 | ||
12 | instantiation | 576, 22, 23 | ||
13 | conjecture | ⊢ | ||
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos | ||||
14 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.posnat_power_of_quotient | ||||
15 | instantiation | 705, 683, 24 | ||
16 | instantiation | 418, 704, 25, 611, 26 | ||
17 | instantiation | 27, 677 | ⊢ | |
18 | instantiation | 28, 677, 29, 696, 30*, 31* | ||
19 | instantiation | 32, 413, 702, 668*, 33* | ||
20 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg | ||||
21 | instantiation | 525, 82 | ||
22 | instantiation | 576, 34, 35 | ||
23 | instantiation | 36, 702, 704, 593, 594, 107, 37, 543, 38, 39* | ||
24 | instantiation | 638, 684, 41 | ||
25 | instantiation | 645 | ⊢ | |
26 | instantiation | 705, 633, 40 | ||
27 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.exponentiated_one | ||||
28 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.posnat_power_of_product | ||||
29 | instantiation | 705, 683, 41 | ||
30 | instantiation | 579, 42, 43, 569 | ⊢ | |
31 | instantiation | 44, 440 | ||
32 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.even_pow_is_even_fn_rev | ||||
33 | instantiation | 579, 45, 46, 47 | ||
34 | instantiation | 331, 48, 49 | ||
35 | instantiation | 534, 702, 704, 593, 197, 594, 677, 470, 459 | ||
36 | conjecture | ⊢ | ||
proveit.numbers.multiplication.distribute_through_abs_sum | ||||
37 | instantiation | 645 | ⊢ | |
38 | instantiation | 705, 683, 50 | ||
39 | instantiation | 540, 470, 51, 52* | ||
40 | instantiation | 705, 620, 53 | ||
41 | instantiation | 705, 500, 54 | ||
42 | instantiation | 55, 696, 677 | ⊢ | |
43 | instantiation | 56, 704, 57, 629, 58 | ⊢ | |
44 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.square_abs_real_simp | ||||
45 | instantiation | 59, 73, 596 | ||
46 | instantiation | 389, 60, 596 | ||
47 | instantiation | 658 | ⊢ | |
48 | instantiation | 61, 62, 63 | ||
49 | instantiation | 576, 64, 65 | ||
50 | instantiation | 705, 690, 66 | ||
51 | instantiation | 705, 683, 67 | ||
52 | instantiation | 576, 68, 69 | ||
53 | instantiation | 441, 70 | ||
54 | instantiation | 525, 413 | ||
55 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.exp_nat_pos_expansion | ||||
56 | conjecture | ⊢ | ||
proveit.core_expr_types.operations.operands_substitution_via_tuple | ||||
57 | instantiation | 71, 704 | ⊢ | |
58 | instantiation | 72 | ⊢ | |
59 | conjecture | ⊢ | ||
proveit.numbers.negation.distribute_neg_through_subtract | ||||
60 | instantiation | 539, 73 | ⊢ | |
61 | conjecture | ⊢ | ||
proveit.numbers.ordering.transitivity_less_eq_less_eq | ||||
62 | instantiation | 74, 103, 156, 684, 75, 104 | ||
63 | instantiation | 76, 106, 77, 78, 79, 80* | ||
64 | instantiation | 81, 82, 83, 84, 85* | ||
65 | instantiation | 287, 642, 122, 230, 86, 87*, 88* | ||
66 | instantiation | 705, 671, 89 | ||
67 | instantiation | 705, 690, 90 | ||
68 | instantiation | 576, 91, 92 | ||
69 | instantiation | 579, 93, 94, 95 | ||
70 | instantiation | 462, 413, 96 | ||
71 | conjecture | ⊢ | ||
proveit.core_expr_types.tuples.range_from1_len_typical_eq | ||||
72 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.reduce_2_repeats | ||||
73 | instantiation | 705, 683, 460 | ⊢ | |
74 | conjecture | ⊢ | ||
proveit.numbers.division.weak_div_from_numer_bound__pos_denom | ||||
75 | instantiation | 97, 642, 247, 98* | ||
76 | conjecture | ⊢ | ||
proveit.numbers.division.weak_div_from_denom_bound__all_pos | ||||
77 | instantiation | 99, 529, 100, 101, 138, 414 | ||
78 | instantiation | 102, 103, 104 | ||
79 | instantiation | 105, 704, 593, 260, 594, 106, 107, 246, 108* | ||
80 | instantiation | 579, 109, 110, 111 | ||
81 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_eq | ||||
82 | instantiation | 112, 113 | ||
83 | instantiation | 528, 116, 117 | ||
84 | instantiation | 114, 679, 504 | ||
85 | instantiation | 337, 696, 115, 116, 117, 118*, 119* | ||
86 | instantiation | 120, 611, 121 | ||
87 | instantiation | 666, 122 | ||
88 | instantiation | 652, 123, 124 | ||
89 | instantiation | 125, 126 | ||
90 | instantiation | 705, 671, 126 | ||
91 | instantiation | 127, 642, 596, 230, 610 | ||
92 | instantiation | 652, 128, 129 | ⊢ | |
93 | instantiation | 667, 614 | ⊢ | |
94 | instantiation | 667, 130 | ||
95 | instantiation | 666, 596 | ||
96 | instantiation | 485, 131 | ||
97 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.triangle_inequality | ||||
98 | instantiation | 652, 132, 133 | ||
99 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_real_pos_closure | ||||
100 | instantiation | 550 | ⊢ | |
101 | instantiation | 705, 345, 134 | ⊢ | |
102 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos | ||||
103 | instantiation | 576, 135, 136 | ||
104 | instantiation | 137, 704, 593, 260, 594, 314, 138, 217, 139* | ||
105 | conjecture | ⊢ | ||
proveit.numbers.multiplication.weak_bound_via_factor_bound | ||||
106 | instantiation | 705, 141, 140 | ⊢ | |
107 | instantiation | 705, 141, 142 | ⊢ | |
108 | instantiation | 652, 143, 144 | ||
109 | instantiation | 652, 145, 146 | ||
110 | instantiation | 658 | ⊢ | |
111 | instantiation | 455, 147 | ||
112 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._alpha_are_complex | ||||
113 | instantiation | 148, 619, 670 | ||
114 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._alpha_summed | ||||
115 | instantiation | 645 | ⊢ | |
116 | instantiation | 705, 683, 149 | ⊢ | |
117 | instantiation | 286, 218, 152, 153 | ||
118 | instantiation | 369, 150 | ⊢ | |
119 | instantiation | 151, 218, 152, 153, 154* | ||
120 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_complex_nonzero_closure_bin | ||||
121 | instantiation | 462, 167, 155 | ||
122 | instantiation | 705, 683, 156 | ||
123 | instantiation | 591, 702, 704, 593, 157, 594, 470, 677, 167 | ||
124 | instantiation | 533, 593, 702, 594, 470, 677, 167 | ||
125 | conjecture | ⊢ | ||
proveit.numbers.negation.rational_nonzero_closure | ||||
126 | instantiation | 158, 159, 291 | ||
127 | conjecture | ⊢ | ||
proveit.numbers.division.mult_frac_cancel_numer_left | ||||
128 | instantiation | 667, 160 | ⊢ | |
129 | instantiation | 667, 161 | ⊢ | |
130 | instantiation | 669, 596 | ||
131 | instantiation | 162, 503, 670, 504 | ||
132 | instantiation | 627, 704, 163, 164, 165, 166 | ||
133 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.add_1_1 | ||||
134 | instantiation | 705, 674, 606 | ⊢ | |
135 | instantiation | 638, 290, 216 | ||
136 | instantiation | 591, 593, 704, 702, 594, 260, 677, 470, 167 | ||
137 | conjecture | ⊢ | ||
proveit.numbers.multiplication.strong_bound_via_factor_bound | ||||
138 | instantiation | 705, 345, 233 | ⊢ | |
139 | instantiation | 168, 704, 593, 260, 594, 677, 470 | ⊢ | |
140 | instantiation | 705, 169, 704 | ⊢ | |
141 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg | ||||
142 | instantiation | 705, 169, 170 | ⊢ | |
143 | instantiation | 591, 704, 593, 260, 458, 594, 677, 470, 459 | ||
144 | instantiation | 652, 171, 172 | ||
145 | instantiation | 667, 173 | ||
146 | instantiation | 520, 677, 174, 175, 176* | ||
147 | instantiation | 652, 177, 178 | ||
148 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._mod_add_closure | ||||
149 | instantiation | 705, 690, 179 | ⊢ | |
150 | instantiation | 398, 180 | ⊢ | |
151 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_frac | ||||
152 | instantiation | 443, 642, 181 | ||
153 | instantiation | 485, 182 | ||
154 | instantiation | 183, 483, 184, 185*, 186*, 187* | ||
155 | instantiation | 267, 188 | ||
156 | instantiation | 705, 500, 189 | ||
157 | instantiation | 645 | ⊢ | |
158 | conjecture | ⊢ | ||
proveit.numbers.division.div_rational_nonzero_closure | ||||
159 | instantiation | 190, 655, 504 | ||
160 | instantiation | 652, 191, 192 | ⊢ | |
161 | instantiation | 667, 193 | ⊢ | |
162 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._scaled_delta_b_not_eq_nonzeroInt | ||||
163 | instantiation | 645 | ⊢ | |
164 | instantiation | 645 | ⊢ | |
165 | instantiation | 369, 194 | ⊢ | |
166 | instantiation | 307, 283, 195* | ||
167 | instantiation | 705, 683, 216 | ||
168 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_zero_any | ||||
169 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg | ||||
170 | instantiation | 705, 196, 517 | ⊢ | |
171 | instantiation | 533, 702, 677, 470, 459 | ||
172 | instantiation | 534, 593, 704, 594, 629, 197, 677, 470, 459, 569* | ||
173 | instantiation | 667, 359 | ||
174 | instantiation | 576, 198, 199 | ||
175 | instantiation | 418, 529, 252, 288, 230, 328 | ||
176 | instantiation | 652, 200, 201 | ||
177 | instantiation | 667, 202 | ||
178 | instantiation | 520, 642, 203, 204, 205* | ||
179 | instantiation | 705, 647, 206 | ⊢ | |
180 | instantiation | 452, 206 | ⊢ | |
181 | instantiation | 539, 207 | ||
182 | instantiation | 331, 208, 209 | ||
183 | conjecture | ⊢ | ||
proveit.trigonometry.complex_unit_circle_chord_length | ||||
184 | instantiation | 576, 426, 396 | ||
185 | instantiation | 652, 210, 211 | ⊢ | |
186 | instantiation | 455, 212 | ||
187 | instantiation | 652, 213, 214 | ||
188 | instantiation | 215, 483, 216, 217 | ||
189 | instantiation | 525, 218 | ||
190 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.nonzero_rational_is_rational_nonzero | ||||
191 | instantiation | 667, 219 | ⊢ | |
192 | instantiation | 669, 470 | ⊢ | |
193 | instantiation | 676, 470 | ⊢ | |
194 | instantiation | 397, 702 | ⊢ | |
195 | instantiation | 220, 221, 222* | ||
196 | conjecture | ⊢ | ||
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat | ||||
197 | instantiation | 645 | ⊢ | |
198 | instantiation | 528, 223, 329 | ||
199 | instantiation | 591, 593, 704, 702, 594, 224, 571, 470, 329 | ||
200 | instantiation | 667, 225 | ||
201 | instantiation | 652, 226, 227 | ||
202 | instantiation | 667, 359 | ||
203 | instantiation | 576, 228, 229 | ||
204 | instantiation | 418, 529, 293, 611, 230, 328 | ||
205 | instantiation | 652, 231, 232 | ||
206 | instantiation | 662, 663, 233 | ⊢ | |
207 | instantiation | 553, 319, 234 | ||
208 | instantiation | 331, 235, 236 | ||
209 | instantiation | 667, 237 | ||
210 | instantiation | 667, 238 | ⊢ | |
211 | instantiation | 622, 319 | ⊢ | |
212 | instantiation | 667, 239 | ||
213 | instantiation | 667, 240 | ||
214 | instantiation | 652, 241, 242 | ||
215 | conjecture | ⊢ | ||
proveit.numbers.ordering.less_is_not_eq | ||||
216 | instantiation | 371, 483, 657, 243 | ||
217 | instantiation | 244, 245, 246 | ||
218 | instantiation | 443, 642, 247 | ||
219 | instantiation | 666, 470 | ⊢ | |
220 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.complex_unit_length | ||||
221 | instantiation | 576, 248, 249 | ||
222 | instantiation | 455, 250 | ||
223 | instantiation | 705, 683, 251 | ⊢ | |
224 | instantiation | 645 | ⊢ | |
225 | instantiation | 292, 338, 252, 571, 470, 329, 583, 572, 471, 294, 253*, 472* | ||
226 | instantiation | 591, 702, 529, 593, 254, 594, 677, 257, 597, 296 | ||
227 | instantiation | 534, 593, 704, 594, 255, 256, 677, 257, 597, 296, 258* | ||
228 | instantiation | 528, 259, 329 | ||
229 | instantiation | 591, 593, 704, 702, 594, 260, 677, 470, 329 | ||
230 | instantiation | 705, 633, 261 | ⊢ | |
231 | instantiation | 667, 262 | ||
232 | instantiation | 652, 263, 264 | ||
233 | instantiation | 705, 674, 517 | ⊢ | |
234 | instantiation | 576, 265, 266 | ||
235 | instantiation | 267, 268 | ||
236 | instantiation | 667, 269 | ||
237 | instantiation | 667, 270 | ||
238 | instantiation | 519, 423 | ⊢ | |
239 | instantiation | 652, 271, 272 | ||
240 | instantiation | 652, 273, 274 | ||
241 | instantiation | 652, 275, 276 | ||
242 | instantiation | 669, 310 | ||
243 | instantiation | 277, 278 | ||
244 | conjecture | ⊢ | ||
proveit.numbers.ordering.transitivity_less_less_eq | ||||
245 | instantiation | 451, 279 | ||
246 | instantiation | 280, 281, 373, 282* | ||
247 | instantiation | 539, 283 | ||
248 | instantiation | 638, 464, 440 | ||
249 | instantiation | 591, 593, 704, 702, 594, 445, 677, 623, 413 | ||
250 | instantiation | 667, 284 | ||
251 | instantiation | 638, 604, 493 | ⊢ | |
252 | instantiation | 550 | ⊢ | |
253 | instantiation | 600, 288, 675, 285* | ⊢ | |
254 | instantiation | 550 | ⊢ | |
255 | instantiation | 645 | ⊢ | |
256 | instantiation | 645 | ⊢ | |
257 | instantiation | 286, 642, 571, 572 | ⊢ | |
258 | instantiation | 287, 677, 642, 610, 288, 654*, 289* | ⊢ | |
259 | instantiation | 705, 683, 290 | ⊢ | |
260 | instantiation | 645 | ⊢ | |
261 | instantiation | 705, 650, 291 | ⊢ | |
262 | instantiation | 292, 338, 293, 677, 470, 329, 583, 521, 471, 294, 563*, 472* | ||
263 | instantiation | 591, 702, 529, 593, 295, 594, 642, 565, 597, 296 | ||
264 | instantiation | 592, 593, 529, 594, 295, 565, 597, 296 | ||
265 | instantiation | 528, 411, 297 | ||
266 | instantiation | 652, 298, 299 | ||
267 | theorem | ⊢ | ||
proveit.logic.equality.not_equals_symmetry | ||||
268 | instantiation | 300, 301, 302, 303* | ||
269 | instantiation | 667, 335 | ||
270 | instantiation | 579, 390, 304, 305 | ||
271 | instantiation | 533, 593, 704, 702, 594, 445, 677, 623, 423, 526 | ||
272 | instantiation | 534, 702, 529, 593, 339, 594, 423, 677, 623, 526 | ||
273 | instantiation | 667, 306 | ||
274 | instantiation | 307, 367, 308* | ||
275 | instantiation | 667, 309 | ||
276 | instantiation | 408, 611, 610, 310, 668* | ||
277 | conjecture | ⊢ | ||
proveit.trigonometry.sine_pos_interval | ||||
278 | instantiation | 311, 483, 644, 342, 312 | ||
279 | instantiation | 313, 314, 414 | ||
280 | conjecture | ⊢ | ||
proveit.trigonometry.sine_linear_bound_nonneg | ||||
281 | instantiation | 315, 342, 316 | ||
282 | instantiation | 652, 317, 318 | ||
283 | instantiation | 553, 319, 320 | ||
284 | instantiation | 652, 321, 322 | ||
285 | instantiation | 626, 571 | ⊢ | |
286 | conjecture | ⊢ | ||
proveit.numbers.division.div_complex_closure | ||||
287 | conjecture | ⊢ | ||
proveit.numbers.division.prod_of_fracs | ||||
288 | instantiation | 705, 633, 323 | ⊢ | |
289 | instantiation | 652, 324, 325 | ⊢ | |
290 | instantiation | 638, 684, 493 | ⊢ | |
291 | instantiation | 705, 687, 326 | ⊢ | |
292 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.real_power_of_products | ||||
293 | instantiation | 550 | ⊢ | |
294 | instantiation | 327, 328 | ||
295 | instantiation | 550 | ⊢ | |
296 | instantiation | 553, 329, 554 | ||
297 | instantiation | 528, 423, 526 | ||
298 | instantiation | 591, 702, 704, 593, 330, 594, 411, 423, 526 | ||
299 | instantiation | 591, 593, 704, 594, 445, 330, 677, 623, 423, 526 | ||
300 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.unit_complex_polar_num_neq_one | ||||
301 | instantiation | 576, 444, 417 | ||
302 | instantiation | 331, 332, 333 | ||
303 | instantiation | 455, 334 | ||
304 | instantiation | 455, 363 | ||
305 | instantiation | 455, 335 | ||
306 | instantiation | 477, 336 | ||
307 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_even | ||||
308 | instantiation | 337, 338, 339, 677, 623, 526, 340*, 341* | ||
309 | instantiation | 534, 702, 704, 593, 376, 594, 677, 623, 459 | ||
310 | instantiation | 705, 683, 342 | ||
311 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.in_IntervalOO | ||||
312 | instantiation | 343, 346, 344 | ||
313 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_real_pos_closure_bin | ||||
314 | instantiation | 705, 345, 664 | ⊢ | |
315 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.nonneg_real_is_real_nonneg | ||||
316 | instantiation | 398, 346 | ||
317 | instantiation | 667, 347 | ||
318 | instantiation | 652, 348, 349 | ||
319 | instantiation | 705, 683, 350 | ⊢ | |
320 | instantiation | 576, 351, 352 | ||
321 | instantiation | 533, 593, 704, 702, 594, 445, 677, 623, 423, 413 | ||
322 | instantiation | 534, 702, 529, 593, 353, 594, 423, 677, 623, 413 | ||
323 | instantiation | 705, 650, 354 | ⊢ | |
324 | instantiation | 627, 704, 355, 356, 668, 357 | ⊢ | |
325 | instantiation | 408, 611, 642, 668*, 569* | ⊢ | |
326 | instantiation | 705, 695, 517 | ⊢ | |
327 | conjecture | ⊢ | ||
proveit.numbers.number_sets.complex_numbers.nonzero_if_in_complex_nonzero | ||||
328 | instantiation | 576, 358, 359 | ||
329 | instantiation | 705, 683, 360 | ||
330 | instantiation | 645 | ⊢ | |
331 | theorem | ⊢ | ||
proveit.logic.equality.sub_left_side_into | ||||
332 | instantiation | 361, 503, 679, 504 | ||
333 | instantiation | 579, 362, 363, 364 | ||
334 | instantiation | 667, 365 | ||
335 | instantiation | 667, 366 | ||
336 | instantiation | 539, 367 | ||
337 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_prod | ||||
338 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.posnat3 | ||||
339 | instantiation | 550 | ⊢ | |
340 | instantiation | 369, 368 | ⊢ | |
341 | instantiation | 369, 370 | ⊢ | |
342 | instantiation | 371, 483, 402, 400 | ||
343 | theorem | ⊢ | ||
proveit.logic.booleans.conjunction.and_if_both | ||||
344 | instantiation | 372, 373, 374 | ||
345 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos | ||||
346 | instantiation | 375, 483, 402, 400 | ||
347 | instantiation | 591, 702, 704, 593, 376, 594, 677, 623, 459 | ||
348 | instantiation | 652, 377, 378 | ||
349 | instantiation | 669, 409 | ||
350 | instantiation | 705, 659, 379 | ⊢ | |
351 | instantiation | 528, 411, 380 | ||
352 | instantiation | 652, 381, 382 | ||
353 | instantiation | 550 | ⊢ | |
354 | instantiation | 705, 687, 383 | ⊢ | |
355 | instantiation | 645 | ⊢ | |
356 | instantiation | 645 | ⊢ | |
357 | instantiation | 666, 571 | ⊢ | |
358 | instantiation | 705, 633, 384 | ||
359 | instantiation | 667, 390 | ||
360 | instantiation | 705, 500, 385 | ||
361 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._non_int_delta_b_diff | ||||
362 | instantiation | 520, 386, 411, 387, 388* | ||
363 | instantiation | 389, 514, 543 | ||
364 | instantiation | 455, 390 | ||
365 | instantiation | 652, 391, 392 | ||
366 | instantiation | 652, 393, 394 | ||
367 | instantiation | 576, 395, 396 | ||
368 | instantiation | 397, 704 | ⊢ | |
369 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_non_neg_elim | ||||
370 | instantiation | 398, 430 | ⊢ | |
371 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real | ||||
372 | conjecture | ⊢ | ||
proveit.numbers.ordering.transitivity_less_eq_less | ||||
373 | instantiation | 399, 483, 402, 400 | ||
374 | instantiation | 401, 402, 403, 498, 404, 405*, 406* | ⊢ | |
375 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound | ||||
376 | instantiation | 645 | ⊢ | |
377 | instantiation | 667, 407 | ||
378 | instantiation | 408, 419, 610, 409, 410* | ||
379 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.e_is_real_pos | ||||
380 | instantiation | 528, 423, 413 | ||
381 | instantiation | 591, 702, 704, 593, 412, 594, 411, 423, 413 | ||
382 | instantiation | 591, 593, 704, 594, 445, 412, 677, 623, 423, 413 | ||
383 | instantiation | 705, 695, 606 | ⊢ | |
384 | instantiation | 705, 620, 414 | ||
385 | instantiation | 525, 415 | ||
386 | instantiation | 576, 416, 417 | ||
387 | instantiation | 418, 704, 445, 611, 419 | ⊢ | |
388 | instantiation | 652, 420, 421 | ||
389 | conjecture | ⊢ | ||
proveit.numbers.addition.commutation | ||||
390 | instantiation | 667, 422 | ||
391 | instantiation | 533, 593, 704, 702, 594, 445, 677, 623, 423, 537 | ||
392 | instantiation | 534, 702, 529, 593, 507, 594, 423, 677, 623, 537 | ||
393 | instantiation | 667, 424 | ⊢ | |
394 | instantiation | 425, 593, 704, 594, 595, 642, 596, 597, 561* | ||
395 | instantiation | 705, 683, 426 | ||
396 | instantiation | 591, 593, 704, 702, 594, 445, 677, 623, 526 | ||
397 | conjecture | ⊢ | ||
proveit.numbers.number_sets.natural_numbers.natural_lower_bound | ||||
398 | conjecture | ⊢ | ||
proveit.numbers.ordering.relax_less | ||||
399 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound | ||||
400 | instantiation | 427, 679, 504 | ||
401 | conjecture | ⊢ | ||
proveit.numbers.addition.strong_bound_via_left_term_bound | ||||
402 | instantiation | 428, 644, 684, 521 | ⊢ | |
403 | instantiation | 638, 607, 483 | ⊢ | |
404 | instantiation | 429, 607, 483, 644, 430, 431 | ⊢ | |
405 | instantiation | 579, 432, 433, 434 | ⊢ | |
406 | instantiation | 652, 435, 436 | ⊢ | |
407 | instantiation | 652, 437, 438 | ||
408 | conjecture | ⊢ | ||
proveit.numbers.division.frac_cancel_left | ||||
409 | instantiation | 705, 683, 439 | ||
410 | instantiation | 676, 623 | ⊢ | |
411 | instantiation | 705, 683, 464 | ⊢ | |
412 | instantiation | 645 | ⊢ | |
413 | instantiation | 705, 683, 440 | ||
414 | instantiation | 441, 442 | ||
415 | instantiation | 443, 543, 514 | ||
416 | instantiation | 705, 683, 444 | ||
417 | instantiation | 591, 593, 704, 702, 594, 445, 677, 623, 537 | ||
418 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_not_eq_zero | ||||
419 | instantiation | 705, 633, 588 | ⊢ | |
420 | instantiation | 667, 446 | ⊢ | |
421 | instantiation | 652, 447, 448 | ||
422 | instantiation | 667, 449 | ||
423 | conjecture | ⊢ | ||
proveit.numbers.number_sets.complex_numbers.i_is_complex | ||||
424 | instantiation | 667, 450 | ⊢ | |
425 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_neg_any | ||||
426 | instantiation | 638, 464, 549 | ||
427 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._scaled_abs_delta_b_floor_diff_interval | ||||
428 | conjecture | ⊢ | ||
proveit.numbers.division.div_real_closure | ||||
429 | conjecture | ⊢ | ||
proveit.numbers.multiplication.strong_bound_via_right_factor_bound | ||||
430 | instantiation | 451, 660 | ⊢ | |
431 | instantiation | 452, 648 | ⊢ | |
432 | instantiation | 652, 453, 454 | ⊢ | |
433 | instantiation | 658 | ⊢ | |
434 | instantiation | 455, 497 | ⊢ | |
435 | instantiation | 667, 497 | ⊢ | |
436 | instantiation | 455, 456, 457* | ⊢ | |
437 | instantiation | 533, 593, 702, 594, 677, 623, 459 | ||
438 | instantiation | 534, 702, 704, 593, 458, 594, 623, 677, 459 | ||
439 | instantiation | 638, 684, 482 | ||
440 | instantiation | 584, 460, 461 | ||
441 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_nonzero_closure | ||||
442 | instantiation | 462, 526, 463 | ||
443 | conjecture | ⊢ | ||
proveit.numbers.addition.add_complex_closure_bin | ||||
444 | instantiation | 638, 464, 555 | ||
445 | instantiation | 645 | ⊢ | |
446 | instantiation | 465, 677, 623, 583, 521, 557, 563* | ⊢ | |
447 | instantiation | 652, 466, 467 | ||
448 | instantiation | 652, 468, 469 | ||
449 | instantiation | 520, 596, 470, 471, 472* | ||
450 | instantiation | 473, 642, 544, 474* | ⊢ | |
451 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos | ||||
452 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos | ||||
453 | instantiation | 652, 475, 476 | ⊢ | |
454 | instantiation | 477, 478 | ⊢ | |
455 | theorem | ⊢ | ||
proveit.logic.equality.equals_reversal | ||||
456 | instantiation | 512, 593, 704, 702, 594, 479, 565, 623 | ⊢ | |
457 | instantiation | 652, 480, 481 | ⊢ | |
458 | instantiation | 645 | ⊢ | |
459 | instantiation | 705, 683, 482 | ||
460 | instantiation | 573, 483, 657, 484 | ⊢ | |
461 | instantiation | 616, 639 | ||
462 | conjecture | ⊢ | ||
proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero | ||||
463 | instantiation | 485, 486 | ||
464 | instantiation | 638, 684, 644 | ⊢ | |
465 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.real_power_of_product | ||||
466 | instantiation | 652, 487, 488 | ||
467 | instantiation | 652, 489, 490 | ||
468 | instantiation | 592, 593, 529, 594, 531, 623, 537, 536 | ||
469 | instantiation | 652, 491, 492 | ||
470 | instantiation | 705, 683, 493 | ⊢ | |
471 | instantiation | 605, 517 | ⊢ | |
472 | instantiation | 494, 677, 562, 583, 521, 495* | ⊢ | |
473 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_neg_left | ||||
474 | instantiation | 666, 544 | ⊢ | |
475 | instantiation | 667, 496 | ⊢ | |
476 | instantiation | 667, 497 | ⊢ | |
477 | conjecture | ⊢ | ||
proveit.numbers.addition.elim_zero_left | ||||
478 | instantiation | 705, 683, 498 | ⊢ | |
479 | instantiation | 645 | ⊢ | |
480 | instantiation | 667, 499 | ⊢ | |
481 | instantiation | 666, 623 | ⊢ | |
482 | instantiation | 705, 500, 501 | ||
483 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.zero_is_real | ||||
484 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval | ||||
485 | conjecture | ⊢ | ||
proveit.numbers.addition.subtraction.nonzero_difference_if_different | ||||
486 | instantiation | 502, 503, 670, 504 | ||
487 | instantiation | 591, 593, 529, 702, 594, 507, 677, 623, 537, 505 | ||
488 | instantiation | 591, 529, 704, 593, 507, 506, 594, 677, 623, 537, 565, 536 | ||
489 | instantiation | 533, 593, 529, 702, 594, 507, 677, 623, 537, 565, 536 | ||
490 | instantiation | 652, 508, 509 | ||
491 | instantiation | 652, 510, 511 | ||
492 | instantiation | 512, 702, 704, 593, 513, 594, 642, 514, 543, 515*, 516* | ||
493 | instantiation | 598, 599, 517 | ⊢ | |
494 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.real_power_of_real_power | ||||
495 | instantiation | 540, 544, 642, 518* | ⊢ | |
496 | instantiation | 519, 565 | ⊢ | |
497 | instantiation | 520, 623, 677, 521, 522* | ⊢ | |
498 | instantiation | 638, 607, 644 | ⊢ | |
499 | instantiation | 523, 694, 699, 524* | ⊢ | |
500 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.real_nonneg_within_real | ||||
501 | instantiation | 525, 526 | ||
502 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._delta_b_not_eq_scaledNonzeroInt | ||||
503 | instantiation | 527, 593, 702, 594 | ⊢ | |
504 | assumption | |||
505 | instantiation | 528, 565, 536 | ⊢ | |
506 | instantiation | 645 | ⊢ | |
507 | instantiation | 550 | ⊢ | |
508 | instantiation | 534, 593, 704, 529, 594, 530, 531, 565, 677, 623, 537, 536 | ||
509 | instantiation | 667, 532 | ⊢ | |
510 | instantiation | 533, 702, 593, 594, 623, 537, 536 | ||
511 | instantiation | 534, 593, 704, 702, 594, 535, 623, 536, 537, 538* | ||
512 | conjecture | ⊢ | ||
proveit.numbers.multiplication.distribute_through_sum | ||||
513 | instantiation | 645 | ⊢ | |
514 | instantiation | 539, 541 | ||
515 | instantiation | 540, 642, 541, 542* | ||
516 | instantiation | 666, 543 | ⊢ | |
517 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._two_pow_t_is_nat_pos | ||||
518 | instantiation | 676, 544 | ⊢ | |
519 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_zero_right | ||||
520 | conjecture | ⊢ | ||
proveit.numbers.division.div_as_mult | ||||
521 | instantiation | 605, 696 | ⊢ | |
522 | instantiation | 652, 545, 546 | ⊢ | |
523 | conjecture | ⊢ | ||
proveit.numbers.addition.rational_pair_addition | ||||
524 | instantiation | 652, 547, 548 | ⊢ | |
525 | conjecture | ⊢ | ||
proveit.numbers.absolute_value.abs_complex_closure | ||||
526 | instantiation | 705, 683, 549 | ||
527 | conjecture | ⊢ | ||
proveit.logic.sets.enumeration.in_enumerated_set | ||||
528 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_complex_closure_bin | ||||
529 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.nat3 | ||||
530 | instantiation | 645 | ⊢ | |
531 | instantiation | 550 | ⊢ | |
532 | instantiation | 576, 551, 552 | ⊢ | |
533 | conjecture | ⊢ | ||
proveit.numbers.multiplication.leftward_commutation | ||||
534 | conjecture | ⊢ | ||
proveit.numbers.multiplication.association | ||||
535 | instantiation | 645 | ⊢ | |
536 | instantiation | 553, 623, 554 | ⊢ | |
537 | instantiation | 705, 683, 555 | ||
538 | instantiation | 556, 623, 657, 583, 557, 558*, 559* | ⊢ | |
539 | conjecture | ⊢ | ||
proveit.numbers.negation.complex_closure | ||||
540 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_neg_right | ||||
541 | instantiation | 705, 683, 617 | ||
542 | instantiation | 652, 560, 561 | ||
543 | instantiation | 705, 683, 586 | ⊢ | |
544 | instantiation | 705, 683, 562 | ⊢ | |
545 | instantiation | 667, 563 | ⊢ | |
546 | instantiation | 564, 623, 565 | ⊢ | |
547 | instantiation | 627, 704, 566, 567, 568, 569 | ⊢ | |
548 | instantiation | 570, 571, 572 | ⊢ | |
549 | instantiation | 573, 574, 607, 575 | ||
550 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq | ||||
551 | instantiation | 576, 577, 578 | ⊢ | |
552 | instantiation | 579, 580, 581, 582 | ⊢ | |
553 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.exp_complex_closure | ||||
554 | instantiation | 705, 683, 583 | ⊢ | |
555 | instantiation | 584, 585, 586 | ||
556 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.product_of_real_powers | ||||
557 | instantiation | 587, 588 | ⊢ | |
558 | instantiation | 626, 623 | ⊢ | |
559 | instantiation | 652, 589, 590 | ⊢ | |
560 | instantiation | 591, 702, 704, 593, 595, 594, 642, 596, 597 | ||
561 | instantiation | 592, 593, 704, 594, 595, 596, 597 | ||
562 | instantiation | 598, 599, 697 | ⊢ | |
563 | instantiation | 600, 611, 675, 601* | ⊢ | |
564 | conjecture | ⊢ | ||
proveit.numbers.multiplication.commutation | ||||
565 | instantiation | 705, 683, 607 | ⊢ | |
566 | instantiation | 645 | ⊢ | |
567 | instantiation | 645 | ⊢ | |
568 | instantiation | 652, 602, 603 | ⊢ | |
569 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.mult_2_2 | ||||
570 | conjecture | ⊢ | ||
proveit.numbers.division.frac_cancel_complete | ||||
571 | instantiation | 705, 683, 604 | ⊢ | |
572 | instantiation | 605, 606 | ⊢ | |
573 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real | ||||
574 | instantiation | 616, 607 | ⊢ | |
575 | instantiation | 608, 679 | ||
576 | theorem | ⊢ | ||
proveit.logic.equality.sub_right_side_into | ||||
577 | instantiation | 609, 642, 610, 611 | ⊢ | |
578 | instantiation | 652, 612, 613 | ⊢ | |
579 | conjecture | ⊢ | ||
proveit.logic.equality.four_chain_transitivity | ||||
580 | instantiation | 667, 614 | ⊢ | |
581 | instantiation | 667, 614 | ⊢ | |
582 | instantiation | 676, 642 | ⊢ | |
583 | instantiation | 705, 690, 615 | ⊢ | |
584 | conjecture | ⊢ | ||
proveit.numbers.addition.add_real_closure_bin | ||||
585 | instantiation | 616, 617 | ||
586 | instantiation | 618, 619 | ⊢ | |
587 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero | ||||
588 | instantiation | 705, 620, 660 | ⊢ | |
589 | instantiation | 667, 621 | ⊢ | |
590 | instantiation | 622, 623 | ⊢ | |
591 | conjecture | ⊢ | ||
proveit.numbers.multiplication.disassociation | ||||
592 | conjecture | ⊢ | ||
proveit.numbers.multiplication.elim_one_any | ||||
593 | axiom | ⊢ | ||
proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||
594 | conjecture | ⊢ | ||
proveit.core_expr_types.tuples.tuple_len_0_typical_eq | ||||
595 | instantiation | 645 | ⊢ | |
596 | instantiation | 705, 683, 639 | ||
597 | instantiation | 705, 683, 640 | ⊢ | |
598 | theorem | ⊢ | ||
proveit.logic.sets.inclusion.unfold_subset_eq | ||||
599 | instantiation | 624, 625 | ⊢ | |
600 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.neg_power_as_div | ||||
601 | instantiation | 626, 677 | ⊢ | |
602 | instantiation | 627, 704, 628, 629, 651, 668 | ⊢ | |
603 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.add_2_2 | ||||
604 | instantiation | 705, 690, 630 | ⊢ | |
605 | conjecture | ⊢ | ||
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos | ||||
606 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.posnat4 | ||||
607 | instantiation | 705, 690, 631 | ⊢ | |
608 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._delta_b_floor_diff_in_interval | ||||
609 | conjecture | ⊢ | ||
proveit.numbers.division.mult_frac_cancel_denom_left | ||||
610 | instantiation | 705, 633, 632 | ⊢ | |
611 | instantiation | 705, 633, 634 | ⊢ | |
612 | instantiation | 667, 635 | ⊢ | |
613 | instantiation | 667, 636 | ⊢ | |
614 | instantiation | 669, 642 | ⊢ | |
615 | instantiation | 705, 698, 637 | ⊢ | |
616 | conjecture | ⊢ | ||
proveit.numbers.negation.real_closure | ||||
617 | instantiation | 638, 639, 640 | ||
618 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._delta_b_is_real | ||||
619 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._best_floor_is_int | ||||
620 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero | ||||
621 | instantiation | 641, 642, 643 | ⊢ | |
622 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.exp_zero_eq_one | ||||
623 | instantiation | 705, 683, 644 | ⊢ | |
624 | theorem | ⊢ | ||
proveit.logic.sets.inclusion.relax_proper_subset | ||||
625 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.nat_pos_within_real | ||||
626 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.complex_x_to_first_power_is_x | ||||
627 | axiom | ⊢ | ||
proveit.core_expr_types.operations.operands_substitution | ||||
628 | instantiation | 645 | ⊢ | |
629 | instantiation | 645 | ⊢ | |
630 | instantiation | 705, 698, 646 | ⊢ | |
631 | instantiation | 705, 647, 648 | ⊢ | |
632 | instantiation | 705, 650, 649 | ⊢ | |
633 | conjecture | ⊢ | ||
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero | ||||
634 | instantiation | 705, 650, 681 | ⊢ | |
635 | instantiation | 667, 651 | ⊢ | |
636 | instantiation | 652, 653, 654 | ⊢ | |
637 | instantiation | 700, 694 | ⊢ | |
638 | conjecture | ⊢ | ||
proveit.numbers.multiplication.mult_real_closure_bin | ||||
639 | instantiation | 705, 690, 655 | ||
640 | instantiation | 705, 690, 656 | ⊢ | |
641 | conjecture | ⊢ | ||
proveit.numbers.addition.subtraction.add_cancel_basic | ||||
642 | instantiation | 705, 683, 657 | ⊢ | |
643 | instantiation | 658 | ⊢ | |
644 | instantiation | 705, 659, 660 | ⊢ | |
645 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq | ||||
646 | instantiation | 705, 703, 661 | ⊢ | |
647 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational | ||||
648 | instantiation | 662, 663, 664 | ⊢ | |
649 | instantiation | 705, 687, 665 | ⊢ | |
650 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero | ||||
651 | instantiation | 666, 677 | ⊢ | |
652 | axiom | ⊢ | ||
proveit.logic.equality.equals_transitivity | ||||
653 | instantiation | 667, 668 | ⊢ | |
654 | instantiation | 669, 677 | ⊢ | |
655 | instantiation | 705, 698, 670 | ||
656 | instantiation | 705, 671, 672 | ⊢ | |
657 | instantiation | 705, 690, 673 | ⊢ | |
658 | axiom | ⊢ | ||
proveit.logic.equality.equals_reflexivity | ||||
659 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.real_pos_within_real | ||||
660 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.pi_is_real_pos | ||||
661 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.nat4 | ||||
662 | conjecture | ⊢ | ||
proveit.numbers.division.div_rational_pos_closure | ||||
663 | instantiation | 705, 674, 675 | ⊢ | |
664 | instantiation | 705, 674, 696 | ⊢ | |
665 | instantiation | 705, 695, 675 | ⊢ | |
666 | conjecture | ⊢ | ||
proveit.numbers.multiplication.elim_one_left | ||||
667 | axiom | ⊢ | ||
proveit.logic.equality.substitution | ||||
668 | instantiation | 676, 677 | ⊢ | |
669 | conjecture | ⊢ | ||
proveit.numbers.division.frac_one_denom | ||||
670 | instantiation | 705, 678, 679 | ||
671 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational | ||||
672 | instantiation | 680, 681, 682 | ⊢ | |
673 | instantiation | 705, 698, 694 | ⊢ | |
674 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos | ||||
675 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.posnat1 | ||||
676 | conjecture | ⊢ | ||
proveit.numbers.multiplication.elim_one_right | ||||
677 | instantiation | 705, 683, 684 | ⊢ | |
678 | instantiation | 685, 686, 701 | ⊢ | |
679 | assumption | |||
680 | conjecture | ⊢ | ||
proveit.numbers.exponentiation.exp_rational_nonzero_closure | ||||
681 | instantiation | 705, 687, 688 | ⊢ | |
682 | instantiation | 700, 689 | ⊢ | |
683 | conjecture | ⊢ | ||
proveit.numbers.number_sets.complex_numbers.real_within_complex | ||||
684 | instantiation | 705, 690, 691 | ⊢ | |
685 | conjecture | ⊢ | ||
proveit.numbers.number_sets.integers.int_interval_within_int | ||||
686 | instantiation | 692, 693, 694 | ⊢ | |
687 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero | ||||
688 | instantiation | 705, 695, 696 | ⊢ | |
689 | instantiation | 705, 706, 697 | ⊢ | |
690 | conjecture | ⊢ | ||
proveit.numbers.number_sets.real_numbers.rational_within_real | ||||
691 | instantiation | 705, 698, 699 | ⊢ | |
692 | conjecture | ⊢ | ||
proveit.numbers.addition.add_int_closure_bin | ||||
693 | instantiation | 700, 701 | ⊢ | |
694 | instantiation | 705, 703, 702 | ⊢ | |
695 | conjecture | ⊢ | ||
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int | ||||
696 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.posnat2 | ||||
697 | axiom | ⊢ | ||
proveit.physics.quantum.QPE._t_in_natural_pos | ||||
698 | conjecture | ⊢ | ||
proveit.numbers.number_sets.rational_numbers.int_within_rational | ||||
699 | instantiation | 705, 703, 704 | ⊢ | |
700 | conjecture | ⊢ | ||
proveit.numbers.negation.int_closure | ||||
701 | instantiation | 705, 706, 707 | ⊢ | |
702 | theorem | ⊢ | ||
proveit.numbers.numerals.decimals.nat1 | ||||
703 | conjecture | ⊢ | ||
proveit.numbers.number_sets.integers.nat_within_int | ||||
704 | conjecture | ⊢ | ||
proveit.numbers.numerals.decimals.nat2 | ||||
705 | theorem | ⊢ | ||
proveit.logic.sets.inclusion.superset_membership_from_proper_subset | ||||
706 | conjecture | ⊢ | ||
proveit.numbers.number_sets.integers.nat_pos_within_int | ||||
707 | conjecture | ⊢ | ||
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos | ||||
*equality replacement requirements |