Proof step 1 from proof mod-mult (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (i0 * i) % (i0 * j) ≠ i % j * i0, 0 < i0, 0 < j, 0 ≤ i ⊦

Rule argument

Additional information

Proof step 2 from proof mod-mult (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  j ≠ 0 ⊦ i % j = i - i / j * j

Rule argument

Additional information

Used simplifier rules: div-mult-01: j ≠ 0, i0 ≠ 0 ⊦ (i * i0) / (j * i0) = i / j; divmod-rew: j ≠ 0 ⊦ i / j * j + i % j = i; ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws) ⊦ i * j - i * j0 = i * (j - j0); (s) ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult lf-03: ⊦ i < j ∧ i = i0 → i0 < j; (forward) from specification int-basic1 ⊦ 0 < i → (i * j < i ↔ j < 1); (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: i0 * j, i0 * i

Proof step 3 from proof mod-mult (previous step) (back to tree)

Lemma mod-rew