---

Step * 1 of Lemma rleq-iff


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)))
BY
{ (Unfold `rsub` 0 THEN (RWO "radd-bdd-diff" 0 THENA Auto) THEN RepUR ``rnonneg2 rminus`` 0) }

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

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
2.  [\%2]  :  regular-seq(x)@i
3.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
4.  [\%1]  :  regular-seq(y)@i
\mvdash{}  rnonneg2(y  -  x)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  ((y  m)  -  x  m)))


By

---

Latex:
(Unfold  `rsub`  0  THEN  (RWO  "radd-bdd-diff"  0  THENA  Auto)  THEN  RepUR  ``rnonneg2  rminus``  0)

---

Home Index