---

Step * 1 1 1 of Lemma rem-mul


1. a : ℤ
2. n : ℤ-o
3. m : ℤ-o
4. (a * n) ÷ m * n ~ a ÷ m
5. a = (((a ÷ m) * m) + (a rem m)) ∈ ℤ
6. (a * n) = (((a ÷ m) * m * n) + (a * n rem m * n)) ∈ ℤ
⊢ (a * n rem m * n) = ((a rem m) * n) ∈ ℤ
BY
{ Mul ⌜n⌝ (-2)⋅ }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  m  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  (a  *  n)  \mdiv{}  m  *  n  \msim{}  a  \mdiv{}  m
5.  a  =  (((a  \mdiv{}  m)  *  m)  +  (a  rem  m))
6.  (a  *  n)  =  (((a  \mdiv{}  m)  *  m  *  n)  +  (a  *  n  rem  m  *  n))
\mvdash{}  (a  *  n  rem  m  *  n)  =  ((a  rem  m)  *  n)


By

---

Latex:
Mul  \mkleeneopen{}n\mkleeneclose{}  (-2)\mcdot{}

---

Home Index