---

Step * of Lemma multiply_eqmod_zero_left

∀m,x,y:ℤ.  ((x ≡ 0 mod m) ⇒ ((x * y) ≡ 0 mod m))
BY
{ (Auto THEN (Assert y ≡ y mod m BY (RelRST THEN Auto))) }

1
1. m : ℤ@i
2. x : ℤ@i
3. y : ℤ@i
4. x ≡ 0 mod m@i
5. y ≡ y mod m
⊢ (x * y) ≡ 0 mod m

---

Latex:

---

Latex:
\mforall{}m,x,y:\mBbbZ{}.    ((x  \mequiv{}  0  mod  m)  {}\mRightarrow{}  ((x  *  y)  \mequiv{}  0  mod  m))


By

---

Latex:
(Auto  THEN  (Assert  y  \mequiv{}  y  mod  m  BY  (RelRST  THEN  Auto)))

---

Home Index