---

Step * of Lemma rneq-int

∀n,m:ℤ.  (r(n) ≠ r(m) ⇐⇒ ¬(n = m ∈ ℤ))
BY
{ (Unfold `rneq` 0 THEN RWO "rless-int" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.    (r(n)  \mneq{}  r(m)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(n  =  m))


By

---

Latex:
(Unfold  `rneq`  0  THEN  RWO  "rless-int"  0  THEN  Auto)

---

Home Index