| all_prime_divisors(binom_coef(2 * i, i)) = ints2 + ints1 + ints0 + i0 ' + ints3, 0 < i, 2 < i, binom_coef(2 * i, i) ≤ (2 * i) ^ (sqrt(2 * i) - 1) * 4 ^ ((2 * i) / 3) * i0 * Π ints3, ∀ j. j ∈ ints0 → (2 * i) / 3 < j ∧ j ≤ i, ∀ j. j ∈ ints1 → sqrt(2 * i) < j ∧ j ≤ (2 * i) / 3, ∀ j. j ∈ ints2 → j ≤ sqrt(2 * i), i0 = i0 ∨ i0 ∈ ints3 → i < i0 ∧ i0 ≤ 2 * i, ∀ j. j ∈ ints3 → i < j ∧ j ≤ 2 * i ⊦ prime(i0) ∧ i < i0 ∧ i0 ≤ 2 * i |
all_prime_divisors(binom_coef(2 * i, i)) = ints2 + ints1 + ints0 + i0 ' + ints3, 1 < i, 2 < i0, 0 < i0, i0 ≤ 2 * i, i < i0, binom_coef(2 * i, i) ≤ (2 * i) ^ (sqrt(2 * i) - 1) * 4 ^ ((2 * i) / 3) * i0 * Π ints3, 2 < i, 0 < i, ∀ j. j ∈ ints2 → j ≤ sqrt(2 * i), ∀ j. j ∈ ints1 → sqrt(2 * i) < j ∧ j ≤ (2 * i) / 3, ∀ j. j ∈ ints0 → (2 * i) / 3 < j ∧ j ≤ i, ∀ j. j ∈ ints3 → i < j ∧ j ≤ 2 * i ⊦ prime(i0)
Used simplifier rules: nummult-ls-02: ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0); from specification int-div%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs%numlslsdel-01: i0 ≠ 0, i0 < i ⊦ (* i) < j → (* i0) < j; from specification int-basic1%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%ls-same-01: ⊦ 0 < i → (i < i * j ↔ 1 < j); from specification int-mult%transitivity: ⊦ i < i0 ∧ i0 < i1 → i < i1; (forward) from specification oelem[intlista]%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs