Proof step 34 from proof middle-coef-max_exp (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  0 < i, 1 < i, 0 < i ^ (i0 + 1), 1 < i ^ (i0 + 1), 0 < fac(2 * j), Σ countFun(1, i0, λ j0. 2 * j / i ^ j0) + i0 < Σ countFun(1, i0, λ j0. (2 * j) / i ^ j0), 0 ≤ i0, 0 < j, 2 * j < i ^ Σ countFun(1, i0, λ i0. (2 * j) / i ^ i0 - 2 * j / i ^ i0), prime(i), i | fac(2 * j) / (fac(j) * fac(j)), 2 * j < i ^ (i0 + 1), i ^ i0 ≤ 2 * j, 0 ≤ j, fac(j) * fac(j) | fac(2 * j), j < i ^ (i0 + 1), 0 < fac(j), 0 ≤ Σ countFun(1, i0, λ i0. (2 * j) / i ^ i0 - 2 * j / i ^ i0), 0 < Σ countFun(1, i0, λ i0. (2 * j) / i ^ i0 - 2 * j / i ^ i0), i0 < Σ countFun(1, i0, λ i0. (2 * j) / i ^ i0 - 2 * j / i ^ i0) ⊦ Σ countFun(1, i0, λ j0. (2 * j) / i ^ j0) = Σ countFun(1, i0, λ j0. 2 * j / i ^ j0)

Rule argument

Additional information

Used simplifier rules: forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%zero-gels: ⊦ i < 0 ∧ 0 ≤ j → ¬ j < i; from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%one: ⊦ 1 * i = i; from specification int-mult%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%ler: ⊦ i ≤ i; from specification int-abs%succ-02: ⊦ i < j + 1 ↔ i ≤ j; from specification int-abs%ls-pos: ⊦ 1 < i ∧ 0 ≤ j → (i ^ j < i ^ j0 ↔ j < j0); from specification int-pot