This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| binomlist-rec | ⊦ 0 ≤ j0 → binom_list(i, i0, j, j0) = binom_list(i, i0, j, j0 - 1) + (binom_coef(j, j0) * i ^ j0 * i0 ^ (j - j0))' | An Axiom |
| binomlist-less | ⊦ j0 < 0 → binom_list(i, i0, j, j0) = [] | An Axiom |
| binomlist-def | ⊦ binom_list(i, i0, j) = binom_list(i, i0, j, j) | An Axiom |
| binom-def | ⊦ 0 ≤ j ∧ j ≤ i → binom_coef(i, j) = fac(i) / (fac(i - j) * fac(j)) | An Axiom |
| binom-less | ⊦ ¬(0 ≤ j ∧ j ≤ i) → binom_coef(i, j) = 0 | An Axiom |
| fac-rec | ⊦ 0 < i → fac(i) = i * fac(i - 1) | An Axiom |
| fac-zero | ⊦ i ≤ 0 → fac(i) = 1 | An Axiom |
| binomlist-def2 | ⊦ binom_list(i, i0, j) = countFun(0, j, λ j0. binom_coef(j, j0) * i ^ j0 * i0 ^ (j - j0)) | An Axiom |
| max_exp-def | ⊦ max_exp(i, j) = n→i(#oc(i, all_prime_divisors(j))) | An Axiom |
| BertrandsPostulate | ⊦ ∀ i. 0 < i → (∃ j. prime(j) ∧ i < j ∧ j ≤ 2 * i) | A User Theorem |
| Binom-theorem | ⊦ 0 ≤ j → (i + i0) ^ j = Σ binom_list(i, i0, j) | A User Theorem |
| Binom-theorem-countFun | ⊦ 0 ≤ j → (i + i0) ^ j = Σ countFun(0, j, λ j0. binom_coef(j, j0) * i ^ j0 * i0 ^ (j - j0)) | A User Theorem |
| bertrand-big-primes | ⊦ (2 * i) / 3 < j ∧ j ≤ i ∧ prime(j) ∧ 2 < i → ¬ j | binom_coef(2 * i, i) | A User Theorem |
| bertrand-estimate | i ≥ 1024 ⊦ ¬ 4 ^ i ≤ 4 ^ ((2 * i) / 3) * (2 * i) ^ sqrt(2 * i) | A User Theorem |
| bertrand-holds-lower | ⊦ ∀ i. 0 < i ∧ i ≤ 2 ^ 10 → (∃ j. prime(j) ∧ i < j ∧ j ≤ 2 * i) | A User Theorem |
| bertrand-middle-coef-smaller | all_prime_divisors(binom_coef(2 * i, i)) = ints + ints0 + ints1 + ints2 ∧ (∀ j. j ∈ ints → j ≤ sqrt(2 * i)) ∧ (∀ j. j ∈ ints0 → sqrt(2 * i) < j ∧ j ≤ (2 * i) / 3) ∧ (∀ j. j ∈ ints1 → (2 * i) / 3 < j ∧ j ≤ i) ∧ (∀ j. j ∈ ints2 → i < j ∧ j ≤ 2 * i), 2 < i ⊦ binom_coef(2 * i, i) ≤ (2 * i) ^ (sqrt(2 * i) - 1) * 4 ^ ((2 * i) / 3) * Π ints2 | A User Theorem |
| bertrand-middle-primes | ∀ j. j ∈ ints0 → sqrt(2 * i) < j ∧ j ≤ (2 * i) / 3, all_prime_divisors(binom_coef(2 * i, i)) = ints + ints0 + ints1, 2 < i ⊦ Π ints0 ≤ 4 ^ ((2 * i) / 3) | A User Theorem |
| bertrand-prime-factors | 1 < i ⊦ ∃ ints, ints0, ints1, ints2. all_prime_divisors(binom_coef(2 * i, i)) = ints + ints0 + ints1 + ints2 ∧ (∀ j. j ∈ ints → j ≤ sqrt(2 * i)) ∧ (∀ j. j ∈ ints0 → sqrt(2 * i) < j ∧ j ≤ (2 * i) / 3) ∧ (∀ j. j ∈ ints1 → (2 * i) / 3 < j ∧ j ≤ i) ∧ (∀ j. j ∈ ints2 → i < j ∧ j ≤ 2 * i) | A User Theorem |
| bertrand-small-primes | ∀ j. j ∈ ints → j ≤ sqrt(2 * i), all_prime_divisors(binom_coef(2 * i, i)) = ints + ints0, 2 < i ⊦ Π ints ≤ (2 * i) ^ (sqrt(2 * i) - 1) | A User Theorem |
| coef-divides-rec | j ≤ i ∧ 0 < j ⊦ j | binom_coef(i - 1, j - 1) * i | A User Theorem |
| coef-divides-rec-lower | ⊦ 0 < j ∧ j ≤ i → j | binom_coef(i, j - 1) * (i + 1 - j) | A User Theorem |
| coef-eq-zero | ⊦ binom_coef(i, j) = 0 ↔ j < 0 ∨ i < j | A User Theorem |
| coef-fac-divides | ⊦ 0 < j ∧ j ≤ i → fac(j) * fac(i - j) | fac(i) | A User Theorem |
| coef-fac-divides-h | fac(j - 1) * fac(i - j) | fac(i - 1), fac(j) * fac(i - 1 + j) | fac(i - 1), 0 < j, j < i, 0 ≤ j, 1 < i, 0 < i ⊦ fac(j) * fac(i - j) | fac(i) | A User Theorem |
| coef-gcd | ⊦ gcd(i, j) = 1 ∧ j ≤ i ∧ 0 ≤ j → i | binom_coef(i, j) | A User Theorem |
| coef-le-2pot | ⊦ 0 < j → binom_coef(2 * j + 1, j) ≤ 2 ^ (2 * j) | A User Theorem |
| coef-le-zero | ⊦ binom_coef(i, j) ≤ 0 ↔ binom_coef(i, j) = 0 | A User Theorem |
| coef-mult-rec | ⊦ 0 < j ∧ j ≤ i → i * binom_coef(i - 1, j - 1) = j * binom_coef(i, j) | A User Theorem |
| coef-mult-rec-lower | ⊦ 0 < j ∧ j ≤ i → binom_coef(i, j) * j = binom_coef(i, j - 1) * (i + 1 - j) | A User Theorem |
| coef-neg | ⊦ j < 0 → binom_coef(i, j) = 0 | A User Theorem |
| coef-neg-03 | ⊦ j < 0 ∧ i ≤ 0 ∧ i ≠ j ∧ i ≠ j + 1 → binom_coef(i, j) = 0 | A User Theorem |
| coef-nls-zero | ⊦ ¬ binom_coef(i, j) < 0 | A User Theorem |
| coef-one | ⊦ 0 < i → binom_coef(i, 1) = i | A User Theorem |
| coef-pred-01 | ⊦ 0 < j → binom_coef(j, j - 1) = j | A User Theorem |
| coef-product-le | ∀ i. i ∈ ints → prime(i) ∧ j + 2 ≤ i ∧ i ≤ j * 2 + 1, ¬ dups(ints), 0 < j ⊦ Π ints ≤ binom_coef(2 * j + 1, j) | A User Theorem |
| coef-rec | ⊦ j ≤ i ∧ 0 < j → binom_coef(i, j) = (binom_coef(i - 1, j - 1) * i) / j | A User Theorem |
| coef-rec-add-01 | ⊦ 0 < j ∧ j ≤ i → binom_coef(i, j) = binom_coef(i - 1, j - 1) + binom_coef(i - 1, j) | A User Theorem |
| coef-rec-add-02 | ⊦ 0 < j ∧ j ≤ i + 1 → binom_coef(i + 1, j) = binom_coef(i, j - 1) + binom_coef(i, j) | A User Theorem |
| coef-rec-lower | ⊦ 0 < j ∧ j ≤ i → binom_coef(i, j) = (binom_coef(i, j - 1) * (i + 1 - j)) / j | A User Theorem |
| coef-same | ⊦ 0 ≤ j → binom_coef(j, j) = 1 | A User Theorem |
| coef-same-01 | ⊦ 0 < j → binom_coef(j, j) = 1 | A User Theorem |
| coef-sub | ⊦ 1 ≤ j ∧ j ≤ i → binom_coef(i, j) - binom_coef(i, j - 1) = (fac(i) * (i + 1 - 2 * j)) / (fac(j) * fac(i + 1 - j)) | A User Theorem |
| coef-sub-mult | ⊦ 1 ≤ j ∧ j ≤ i → (binom_coef(i, j) - binom_coef(i, j - 1)) * fac(j) * fac(i + 1 - j) = fac(i) * (i + 1 - 2 * j) | A User Theorem |
| coef-succ | ⊦ 0 ≤ j → binom_coef(j + 1, j) = j + 1 | A User Theorem |
| coef-switch | ⊦ 0 ≤ j ∧ j ≤ i → binom_coef(i, j) = binom_coef(i, i - j) | A User Theorem |
| coef-zero | ⊦ 0 ≤ i → binom_coef(i, 0) = 1 | A User Theorem |
| countFun-add | ⊦ 0 < j1 ∧ j1 ≤ i1 → countFun(j1, i1, λ j0. binom_coef(i1 + 1, j0) * i ^ j0 * i0 ^ (i1 + 1 - j0)) = countFun(j1, i1, λ j0. binom_coef(i1, j0 - 1) * i ^ j0 * i0 ^ (i1 + 1 - j0) + binom_coef(i1, j0) * i ^ j0 * i0 ^ (i1 + 1 - j0)) | A User Theorem |
| countFun-pot | ⊦ Σ countFun(i2, i1, λ j0. i0 * binom_coef(i1, j0) * i ^ j0 * i0 ^ (i1 - j0)) = Σ countFun(i2, i1, λ j0. binom_coef(i1, j0) * i ^ j0 * i0 ^ (i1 + 1 - j0)) | A User Theorem |
| countFun-pot-01 | ⊦ 0 < i2 → countFun(i2, i1, λ j0. binom_coef(i1, j0 - 1) * i ^ j0 * i0 ^ (i1 + 1 - j0)) = countFun(i2, i1, λ j0. i * binom_coef(i1, j0 - 1) * i ^ (j0 - 1) * i0 ^ (i1 - (j0 - 1))) | A User Theorem |
| countFun-shift | ⊦ Σ countFun(i2, i1 - 1, λ j0. i * binom_coef(i1, j0) * i ^ j0 * i0 ^ (i1 - j0)) = Σ countFun(i2 + 1, i1, λ j0. i * binom_coef(i1, j0 - 1) * i ^ (j0 - 1) * i0 ^ (i1 - (j0 - 1))) | A User Theorem |
| divides-pot | ⊦ 0 < j ∧ i ≠ 0 → i | (i * i0) ^ j | A User Theorem |
| divides-sum | ⊦ (∀ j. j ∈ ints → i | j) → i | Σ ints | A User Theorem |
| est-4-big | (2 * i) / 3 < j, j ≤ i, 2 < i, 2 * i < j * j ⊦ (2 * i) / j = 2 * i / j | A User Theorem |
| est-4-big-01 | j ≤ 2 * i % j, 2 * i < j * j, 2 < i, j ≤ i, (2 * i) / 3 < j ⊦ | A User Theorem |
| est-4-big-02 | j ≤ 2 * i % j, 2 < i, j ≤ i, (2 * i) / 3 < j, j ≠ 2, j ≠ 3 ⊦ | A User Theorem |
| fac-add | ⊦ 0 ≤ i ∧ 0 ≤ j → fac(i + j) = fac(i) * Π countFun(1, j, λ j0. i + j0) | A User Theorem |
| fac-divides | ⊦ i ≤ j ∧ 0 ≤ i → fac(j - i) * fac(i) | fac(j) | A User Theorem |
| fac-le | ⊦ 0 < i ∧ 0 < j → (fac(i) ≤ fac(j) ↔ i ≤ j) | A User Theorem |
| fac-le-one | ⊦ fac(i) ≤ 1 ↔ i ≤ 1 | A User Theorem |
| fac-le-zero | ⊦ i * fac(j) ≤ 0 ↔ i ≤ 0 | A User Theorem |
| fac-ls-zero | ⊦ i * fac(j) < 0 ↔ i < 0 | A User Theorem |
| fac-not-neg | ⊦ ¬ fac(i) < 0 | A User Theorem |
| fac-not-zero | ⊦ fac(i) * fac(j) ≠ 0 | A User Theorem |
| fac-one | ⊦ fac(1) = 1 | A User Theorem |
| fac-pos | ⊦ ¬ fac(i) < 1 | A User Theorem |
| fac-pos-01 | ⊦ ¬ fac(i) ≤ 0 | A User Theorem |
| fac-zero-01 | ⊦ i < 0 → fac(i) = 1 | A User Theorem |
| fac-zero-02 | ⊦ fac(i) ≠ 0 | A User Theorem |
| max_exp-div | ⊦ 0 < j ∧ 0 < j0 ∧ prime(i) ∧ j0 | j → max_exp(i, j / j0) = max_exp(i, j) - max_exp(i, j0) | A User Theorem |
| max_exp-div-not | ⊦ ∃ i, j, j0. 0 < j ∧ 0 < j0 ∧ prime(i) ∧ ¬ j0 | j ∧ max_exp(i, j / j0) ≠ max_exp(i, j) - max_exp(i, j0) | A User Theorem |
| max_exp-divides | ⊦ 0 < j ∧ prime(i) → i ^ max_exp(i, j) | j ∧ ¬ i | j / i ^ max_exp(i, j) | A User Theorem |
| max_exp-fac-01 | ⊦ prime(i) ∧ 0 ≤ j0 ∧ j0 < i → max_exp(i, fac(i + j0)) = 1 | A User Theorem |
| max_exp-fac-add | ⊦ prime(i) ∧ 0 < j ∧ 0 ≤ j0 ∧ j0 < i → max_exp(i, fac(i * j + j0)) = max_exp(i, fac(i * j)) | A User Theorem |
| max_exp-fac-gen | ⊦ prime(i) ∧ 0 < j ∧ 0 ≤ i0 ∧ j < i ^ i0 → max_exp(i, fac(j)) = Σ countFun(1, i0, λ j0. j / i ^ j0) | A User Theorem |
| max_exp-fac-gen-stronger | ⊦ prime(i) ∧ 0 < j ∧ 0 ≤ i0 ∧ j < i ^ i0 → max_exp(i, fac(j)) = Σ countFun(1, i0 - 1, λ j0. j / i ^ j0) | A User Theorem |
| max_exp-fac-rec | ⊦ prime(i) ∧ 0 < j ∧ 0 ≤ j0 ∧ j0 < i → max_exp(i, fac(i * j + j0)) = j + max_exp(i, fac(j)) | A User Theorem |
| max_exp-fac-same | ⊦ prime(i) → max_exp(i, fac(i)) = 1 | A User Theorem |
| max_exp-fac-smaller | ⊦ prime(i) ∧ 0 < j ∧ j < i → max_exp(i, fac(j)) = 0 | A User Theorem |
| max_exp-lez | ⊦ max_exp(i, i0) ≤ 0 ↔ max_exp(i, i0) = 0 | A User Theorem |
| max_exp-mult | ⊦ 0 < j ∧ 0 < j0 ∧ prime(i) → max_exp(i, j * j0) = max_exp(i, j) + max_exp(i, j0) | A User Theorem |
| max_exp-mult-01 | ⊦ prime(i) ∧ 0 < j ∧ 0 < j0 → max_exp(i, j * j0) = max_exp(i, j) + max_exp(i, j0) | A User Theorem |
| max_exp-not-div | ⊦ ¬ i | j ∧ prime(i) ∧ 0 < j0 ∧ 0 < j → max_exp(i, j * j0) = max_exp(i, j0) | A User Theorem |
| max_exp-not-neg | ⊦ max_exp(i, i0) ≠ ~1 | A User Theorem |
| max_exp-one | ⊦ prime(i) → max_exp(i, 1) = 0 | A User Theorem |
| max_exp-pos | ⊦ 0 ≤ max_exp(i, j) | A User Theorem |
| max_exp-pos-01 | ⊦ ¬ max_exp(i0, j0) + max_exp(i, j) < 0 | A User Theorem |
| max_exp-pos-02 | ⊦ 0 < max_exp(i, j) ↔ max_exp(i, j) ≠ 0 | A User Theorem |
| max_exp-pos-03 | ⊦ max_exp(i0, j0) + max_exp(i, j) ≤ 0 ↔ max_exp(i0, j0) = 0 ∧ max_exp(i, j) = 0 | A User Theorem |
| max_exp-pos-04 | ⊦ ¬ max_exp(i, j) < 0 | A User Theorem |
| max_exp-primes-two | ⊦ max_exp(i, j) < 2 → all_prime_divisors(j) ≠ ints + i ' + ints0 + i ' + ints1 | A User Theorem |
| max_exp-rec | ⊦ prime(i) ∧ i | j ∧ 0 < j → max_exp(i, j) = max_exp(i, j / i) + 1 | A User Theorem |
| max_exp-same | ⊦ prime(i) → max_exp(i, i) = 1 | A User Theorem |
| max_exp-smaller | ⊦ prime(i) ∧ 0 < j ∧ j < i → max_exp(i, j) = 0 | A User Theorem |
| max_exp-zero | ⊦ prime(i) ∧ 0 < j0 ∧ j0 < i → max_exp(i, i + j0) = 0 | A User Theorem |
| max_exp-zero-01 | ⊦ ¬ i | j ∧ prime(i) ∧ 0 < j → max_exp(i, j) = 0 | A User Theorem |
| max_exp-zero-02 | ⊦ prime(i) ∧ 0 < i0 → (max_exp(i, i0) = 0 ↔ ¬ i | i0) | A User Theorem |
| middle-coef-divides-not | ⊦ 2 * i < j ∧ prime(j) ∧ 0 < i → ¬ j | binom_coef(2 * i, i) | A User Theorem |
| middle-coef-larger | 0 ≤ i ⊦ binom_coef(2 * i, i) ≥ 4 ^ i / (2 * i + 1) | A User Theorem |
| middle-coef-larger-stronger | 0 < i ⊦ binom_coef(2 * i, i) ≥ 4 ^ i / (2 * i) | A User Theorem |
| middle-coef-larger-strongest | 0 < i ⊦ binom_coef(2 * i, i) * 2 * i ≥ 4 ^ i | A User Theorem |
| middle-coef-largest | ⊦ j ≤ 2 * i ∧ 0 ≤ j → ¬ binom_coef(2 * i, i) < binom_coef(2 * i, j) | A User Theorem |
| middle-coef-largest-01 | ⊦ j < i ∧ 0 ≤ j → ¬ binom_coef(2 * i, i) < binom_coef(2 * i, j) | A User Theorem |
| middle-coef-max_exp | i | binom_coef(2 * j, j), prime(i), 0 < j ⊦ i ^ max_exp(i, binom_coef(2 * j, j)) ≤ 2 * j | A User Theorem |
| middle-coef-max_exp-big-primes | ⊦ (2 * i) / 3 < j ∧ j ≤ i ∧ prime(j) ∧ 2 < i → max_exp(j, binom_coef(2 * i, i)) = 0 | A User Theorem |
| middle-coef-max_exp-equality | i ^ i0 ≤ 2 * j, 2 * j < i ^ (i0 + 1), 0 ≤ i0, prime(i), 0 < j ⊦ max_exp(i, binom_coef(2 * j, j)) = Σ countFun(1, i0, λ i0. (2 * j) / i ^ i0 - 2 * j / i ^ i0) | A User Theorem |
| middle-coef-max_exp-le | i ^ i0 ≤ 2 * j, 2 * j < i ^ (i0 + 1), 0 ≤ i0, prime(i), 0 < j ⊦ max_exp(i, binom_coef(2 * j, j)) ≤ i0 | A User Theorem |
| middle-coef-max_exp-stronger | prime(i), 0 < j ⊦ i ^ max_exp(i, binom_coef(2 * j, j)) ≤ 2 * j | A User Theorem |
| middle-coef-not-one | ⊦ 0 < i → binom_coef(2 * i, i) ≠ 1 | A User Theorem |
| middle-coef-not-one-01 | ⊦ 0 < i → ¬ binom_coef(2 * i, i) < 2 | A User Theorem |
| prime-divides-coef | ⊦ j + 2 ≤ j0 ∧ j0 ≤ j * 2 + 1 ∧ prime(j0) ∧ 0 < j → j0 | binom_coef(2 * j + 1, j) | A User Theorem |
| prime-divides-pot | ⊦ i * j = i0 ^ j0 ∧ prime(i) ∧ 0 ≤ j0 → i | i0 | A User Theorem |
| prime-divides-pot-01 | ⊦ prime(i) ∧ 0 < j → (i | i0 ^ j ↔ i | i0) | A User Theorem |
| prime-fac-divides | ⊦ prime(i) ∧ i < j ∧ 0 < j → i | fac(j) | A User Theorem |
| prime-fac-divides-01 | ⊦ prime(i) → i | fac(i) | A User Theorem |
| prime-fac-divides-not | ⊦ prime(i) ∧ j < i ∧ 0 < j → ¬ i | fac(j) | A User Theorem |
| prime-pot-eq | ⊦ prime(i) ∧ 0 < i0 ∧ 0 < i1 ∧ ¬ i | j ∧ ¬ i | j0 → (i ^ i0 * j = i ^ i1 * j0 ↔ i ^ i0 = i ^ i1 ∧ j = j0) | A User Theorem |
| prime-product | primes(ints), max(ints) ≤ i, ¬ dups(ints) ⊦ Π ints ≤ 4 ^ i | A User Theorem |
| prime-product-between | ⊦ primes(ints) ∧ j + 2 ≤ min(ints) ∧ max(ints) ≤ j * 2 + 1 ∧ ¬ dups(ints) ∧ 0 < j → Π ints ≤ 4 ^ j | A User Theorem |
| primes-divide | ¬ dups(ints), ∀ j. j ∈ ints → prime(j) ∧ j | i, 0 < i ⊦ Π ints ≤ i | A User Theorem |
| product-all-elems-le | ∀ i. i ∈ ints → 0 < i ∧ i ≤ i0 ⊦ Π ints ≤ i0 ^ n→i(# ints) | A User Theorem |
| product-pot-no-dups | ∀ i. i ∈ ints → 0 < i ∧ i ^ n→i(#oc(i, ints)) ≤ j ⊦ Π ints ≤ j ^ n→i(# rmdup(ints)) | A User Theorem |
| product-pot-rec | ⊦ i ∈ ints → Π ints = i ^ n→i(#oc(i, ints)) * Π(ints -l i) | A User Theorem |
| small-primes | ⊦ prime(2) ∧ prime(3) ∧ prime(5) ∧ prime(7) ∧ prime(13) ∧ prime(23) ∧ prime(43) ∧ prime(83) ∧ prime(163) ∧ prime(317) ∧ prime(631) ∧ prime(1259) | A User Theorem |