---

Step * of Lemma add_reduce_eqmod

∀m,x,y:ℤ.  ((x + y) ≡ x mod m ⇐⇒ y ≡ 0 mod m)
BY
{ Auto }

1
1. m : ℤ
2. x : ℤ
3. y : ℤ
4. (x + y) ≡ x mod m
⊢ y ≡ 0 mod m

2
1. m : ℤ
2. x : ℤ
3. y : ℤ
4. y ≡ 0 mod m
⊢ (x + y) ≡ x mod m

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index