---

Step * 2 1 of Lemma add_reduce_eqmod


1. m : ℤ
2. x : ℤ
3. y : ℤ
4. y ≡ 0 mod m
5. x ≡ x mod m
⊢ (x + y) ≡ x mod m
BY
{ (FLemma `add_functionality_wrt_eqmod` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index