---

Step * 1 of Lemma rnonneg-iff


1. [x] : ℝ
2. rnonneg(x)@i
3. n : ℕ+@i
⊢ ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
BY
{ (With ⌜n⌝ (D 0)⋅
   THEN Auto
   THEN (With ⌜m⌝ (D 2)⋅ THENA Auto)
   THEN (Using [`n',⌜n⌝] (FLemma `mul_preserves_le` [-1])⋅ THENA Auto)
   THEN RWO "-1<" 0
   THEN Auto') }

---

Latex:

---

Latex:

1.  [x]  :  \mBbbR{}
2.  rnonneg(x)@i
3.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  (x  m)))


By

---

Latex:
(With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)
  THEN  (Using  [`n',\mkleeneopen{}n\mkleeneclose{}]  (FLemma  `mul\_preserves\_le`  [-1])\mcdot{}  THENA  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto')

---

Home Index