---

Step * of Lemma rless-iff-rleq

∀x,y:ℝ.  (x < y ⇐⇒ ∃m:ℕ+. (x ≤ (y - (r1/r(m)))))
BY
{ (Auto THEN ExRepD) }

1
1. x : ℝ
2. y : ℝ
3. x < y
⊢ ∃m:ℕ+. (x ≤ (y - (r1/r(m))))

2
1. x : ℝ
2. y : ℝ
3. m : ℕ+
4. x ≤ (y - (r1/r(m)))
⊢ x < y

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (x  <  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}m:\mBbbN{}\msupplus{}.  (x  \mleq{}  (y  -  (r1/r(m)))))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index