---

Step * of Lemma rem_mul

∀[x,y:ℕ]. ∀[m:ℕ+].  ((x * y rem m) = ((x rem m) * (y rem m) rem m) ∈ ℤ)
BY
{ (Auto
   THEN ((InstLemma `div_rem_sum` [⌜x⌝;⌜m⌝]⋅ THENA Auto) THEN (RW (AddrC [2] (SweepUpC (HypC (-1)))) 0 THENA Auto))
   THEN (InstLemma `div_rem_sum` [⌜y⌝;⌜m⌝]⋅ THENA Auto)
   THEN (RW (AddrC [2] (SweepUpC (HypC (-1)))) 0 THENA Auto)
   THEN (RW IntNormC 0 THENA Auto)) }

1
1. x : ℕ
2. y : ℕ
3. m : ℕ+
4. x = (((x ÷ m) * m) + (x rem m)) ∈ ℤ
5. y = (((y ÷ m) * m) + (y rem m)) ∈ ℤ
⊢ (((x rem m) * (y rem m)) + (m * (x ÷ m) * (y rem m)) + (m * (y ÷ m) * (x rem m)) + (m * m * (x ÷ m) * (y ÷ m)) rem m)
= ((x rem m) * (y rem m) rem m)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbN{}].  \mforall{}[m:\mBbbN{}\msupplus{}].    ((x  *  y  rem  m)  =  ((x  rem  m)  *  (y  rem  m)  rem  m))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RW  (AddrC  [2]  (SweepUpC  (HypC  (-1))))  0  THENA  Auto)
              )
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (SweepUpC  (HypC  (-1))))  0  THENA  Auto)
  THEN  (RW  IntNormC  0  THENA  Auto))

---

Home Index