---

Step * of Lemma neg-approx-of-nonneg-real

∀x:ℝ. ((r0 ≤ x) ⇒ (∀n:ℕ+. (((x n) ≤ 0) ⇒ (|x n| ≤ 2))))
BY
{ (Auto
   THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜n⌝]⋅ THENA Auto)
   THEN (RWO "rabs-difference-bound-rleq" (-1) THENA Auto)
   THEN D -1) }

1
1. x : ℝ
2. r0 ≤ x
3. n : ℕ+
4. (x n) ≤ 0
5. ((x within 1/n) - (r1/r(n))) ≤ x
6. x ≤ ((x within 1/n) + (r1/r(n)))
⊢ |x n| ≤ 2

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((r0  \mleq{}  x)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  (((x  n)  \mleq{}  0)  {}\mRightarrow{}  (|x  n|  \mleq{}  2))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rabs-difference-bound-rleq"  (-1)  THENA  Auto)
  THEN  D  -1)

---

Home Index