---

Step * 1 1 of Lemma rleq-iff


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)))
BY
{ (D 0 THEN (D 0 THENA Auto) THEN RepeatFor 3 (ParallelLast) THEN Auto) }

---

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{}  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  ((y  m)  +  (-(x  m)))))
\mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  ((y  m)  -  x  m)))


By

---

Latex:
(D  0  THEN  (D  0  THENA  Auto)  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index