---

Step * of Lemma rleq-iff

∀x,y:ℝ.  (x ≤ y ⇐⇒ ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * ((y m) - x m))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D -1 THEN D 1 THEN Unfold `rleq` 0 THEN (RWO "rnonneg-iff" 0 THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ@i
2. [%2] : regular-seq(x)@i
3. y : ℕ+ ⟶ ℤ@i
4. [%1] : regular-seq(y)@i
⊢ rnonneg2(y - x) ⇐⇒ ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * ((y m) - x m)))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  ((y  m)  -  x  m))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  D  1
  THEN  Unfold  `rleq`  0
  THEN  (RWO  "rnonneg-iff"  0  THENA  Auto))

---

Home Index