---

Step * of Lemma modulus-equal-iff-eqmod

∀x,y:ℤ. ∀m:ℕ+.  ((x mod m) = (y mod m) ∈ ℤ ⇐⇒ x ≡ y mod m)
BY
{ ((InstLemma `modulus-equal` [] THEN Fold `eqmod` (-1)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.  \mforall{}m:\mBbbN{}\msupplus{}.    ((x  mod  m)  =  (y  mod  m)  \mLeftarrow{}{}\mRightarrow{}  x  \mequiv{}  y  mod  m)


By

---

Latex:
((InstLemma  `modulus-equal`  []  THEN  Fold  `eqmod`  (-1))  THEN  Auto)

---

Home Index