| 0 ≤ i1, 2 ≤ i0 * i1, 0 < i0, 2 < i0 * i1, 1 < i1, 0 < i1, i1 ≤ i0, 1 < i0, 0 ≤ i0, j | i1, prime(j), j * j ≤ i1, j * j ≤ i0, ∀ j. prime(j) ∧ j * j ≤ i0 * i1 → ¬ j | i0 * i1, ∀ i2. i→n(i2) < i→n(i0 * i1) → 0 < i2 ∧ 1 < i2 ∧ (∀ j. prime(j) ∧ j * j ≤ i2 → ¬ j | i2) → prime(i2) ⊦ prime(i1) |
Used simplifier rules: divides-mult-01: ⊦ i | j → i | j * j0;%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%ls-same: ⊦ 0 < i → (i * j < i ↔ j < 1); from specification int-mult%bet-01: ⊦ 0 ≤ i → (i < 1 ↔ i = 0); from specification int-abs%numlslsdel-01: i0 ≠ 0, i0 < i ⊦ (* i) < j → (* i0) < j; from specification int-basic1%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs Used terms: j