---

Step * 1 of Lemma multiply_eqmod_zero_left


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
BY
{ (FLemma `multiply_functionality_wrt_eqmod` [-2;-1] THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}@i
2.  x  :  \mBbbZ{}@i
3.  y  :  \mBbbZ{}@i
4.  x  \mequiv{}  0  mod  m@i
5.  y  \mequiv{}  y  mod  m
\mvdash{}  (x  *  y)  \mequiv{}  0  mod  m


By

---

Latex:
(FLemma  `multiply\_functionality\_wrt\_eqmod`  [-2;-1]  THEN  Auto)

---

Home Index