---

Step * of Lemma rless-int

∀n,m:ℤ.  (r(n) < r(m) ⇐⇒ n < m)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``rless int-to-real`` 0 THEN Auto) }

1
1. n : ℤ@i
2. m : ℤ@i
3. ∃n@0:{ℕ+| (2 * n@0 * n) + 4 < 2 * n@0 * m}@i
⊢ n < m

2
1. n : ℤ@i
2. m : ℤ@i
3. n < m@i
⊢ ∃n@0:{ℕ+| (2 * n@0 * n) + 4 < 2 * n@0 * m}

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``rless  int-to-real``  0  THEN  Auto)

---

Home Index