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