---

Step * 2 1 1 of Lemma infinitesmal-zero


1. x : ℝ
2. k : ℕ+
3. |x| ≤ (r1/r(k))
⊢ rnonneg2(λn.((2 * n) - k * |x n|))
BY
{ ((Assert r(k) ≠ r0 BY
          (BLemma `rneq-int` THEN Auto))
   THEN (nRMul ⌜r(k)⌝ (-2)⋅ THENA (BLemma `rleq-int` THEN Auto))
   THEN Unfold `rleq` (-2)) }

1
1. x : ℝ
2. k : ℕ+
3. rnonneg(r1 - r(k) * |x|)
4. r(k) ≠ r0
⊢ rnonneg2(λn.((2 * n) - k * |x n|))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  k  :  \mBbbN{}\msupplus{}
3.  |x|  \mleq{}  (r1/r(k))
\mvdash{}  rnonneg2(\mlambda{}n.((2  *  n)  -  k  *  |x  n|))


By

---

Latex:
((Assert  r(k)  \mneq{}  r0  BY
                (BLemma  `rneq-int`  THEN  Auto))
  THEN  (nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  (-2)\mcdot{}  THENA  (BLemma  `rleq-int`  THEN  Auto))
  THEN  Unfold  `rleq`  (-2))

---

Home Index