| j < i / j, 0 < i / j, 0 ≤ i / j, j0 < i / j, j0 | i / j, prime(j0), j < i, ∃ i0. j * i0 = i, prime(j), 0 < i, 0 ≤ i, 2 ≤ i, j < j0, 2 ≤ i / j, j + 1 < i / j, ∀ j1. j0 < j1 ∧ j1 < i / j ∧ prime(j1) → ¬ j1 | i / j, ∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i ⊦ prime(i / j), prime(i) |
1 < j0, 0 < j0, 0 < j, j + 1 < i0, 2 ≤ i0, j < j0, 2 ≤ j * i0, prime(j), prime(j0), j0 | i0, j0 < i0, 0 ≤ i0, j < i0, 0 < i0, 2 < i0, ∀ j1. j0 < j1 ∧ j1 < i0 ∧ prime(j1) → ¬ j1 | i0, ∀ j0. j < j0 ∧ j0 < j * i0 ∧ prime(j0) → ¬ j0 | j * i0 ⊦ prime(i0), prime(j * i0)
Used simplifier rules: lst-03: ⊦ i + j < i0 ∧ ¬ j < j0 → i + j0 < i0; from specification int-basic2%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs%numlsledel-01: i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; from specification int-abs%ls-same-01: ⊦ 0 < i → (i < i * j ↔ 1 < j); 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%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%zero-ge: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); from specification int-mult%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%div-mult-03: j ≠ 0 ⊦ (i * j) / j = i; from specification int-div%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%zero-left: ⊦ 0 * i = 0; from specification int-mult