Proof step 5 from proof div-ngr-zero (previous step)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%modzero-02: ⊦ i < 0 ∧ j0 < j ∧ 0 < j → i * j + j0 < 0; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%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%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%ls-02: ⊦ i < i + j ↔ 0 < j; from specification int-basic2%zero-gr-add: ⊦ 0 < j → (0 < i * j + j ↔ 0 ≤ i); from specification int-mult%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%zero-left: ⊦ 0 * i = 0; from specification int-mult%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%numlslsdel-03: ⊦ i < j ∧ i0 ≠ 0 ∧ i0 ≤ i → (* i0) < j; from specification int-abs%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs Used formulas: i0 = 0