---

Step * of Lemma rem-mul

∀[a:ℤ]. ∀[n,m:ℤ-o].  ((a * n rem m * n) = ((a rem m) * n) ∈ ℤ)
BY
{ (InstLemma `div-mul-cancel` [] THEN RepeatFor 3 (ParallelLast')) }

1
1. a : ℤ
2. n : ℤ-o
3. m : ℤ-o
4. (a * n) ÷ m * n ~ a ÷ m
⊢ (a * n rem m * n) = ((a rem m) * n) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n,m:\mBbbZ{}\msupminus{}\msupzero{}].    ((a  *  n  rem  m  *  n)  =  ((a  rem  m)  *  n))


By

---

Latex:
(InstLemma  `div-mul-cancel`  []  THEN  RepeatFor  3  (ParallelLast'))

---

Home Index