---

Step * 1 of Lemma rem-mul


1. a : ℤ
2. n : ℤ-o
3. m : ℤ-o
4. (a * n) ÷ m * n ~ a ÷ m
⊢ (a * n rem m * n) = ((a rem m) * n) ∈ ℤ
BY
{ ((InstLemma `div_rem_sum` [⌜a⌝;⌜m⌝]⋅ THENA Auto) THEN (InstLemma `div_rem_sum` [⌜a * n⌝;⌜m * n⌝]⋅ THENA Auto)) }

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 * n) ÷ m * n) * m * n) + (a * n rem m * n)) ∈ ℤ
⊢ (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
\mvdash{}  (a  *  n  rem  m  *  n)  =  ((a  rem  m)  *  n)


By

---

Latex:
((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a  *  n\mkleeneclose{};\mkleeneopen{}m  *  n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index