---

Step * of Lemma add_eqmod_zero

∀m,x,y:ℤ.  ((x ≡ 0 mod m) ⇒ (y ≡ 0 mod m) ⇒ ((x + y) ≡ 0 mod m))
BY
{ (Auto THEN FLemma `add_functionality_wrt_eqmod` [-1;-2] THEN Auto) }

---

Latex:

---

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


By

---

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

---

Home Index