---

Step * of Lemma real-upper-bound

∀[x:ℝ]. ∀[n:ℕ+].  (x ≤ r((((x n) + 1) ÷ 2 * n) + 1))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜n⌝]⋅ THENA Auto)
   THEN (RWO "rabs-difference-bound-rleq" (-1) THENA Auto)
   THEN D -1
   THEN (RWO "-1" 0 THENA Auto)
   THEN RepUR ``rational-approx`` 0
   THEN (RWO  "int-rdiv-req" 0 THENA Auto)
   THEN (nRMul ⌜r(2 * n)⌝ 0⋅ THENA Auto)) }

1
1. x : ℝ
2. n : ℕ+
3. ((x within 1/n) - (r1/r(n))) ≤ x
4. x ≤ ((x within 1/n) + (r1/r(n)))
⊢ r(2 + (x n)) ≤ r((2 * n) + (2 * (((x n) + 1) ÷ 2 * n) * n))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (x  \mleq{}  r((((x  n)  +  1)  \mdiv{}  2  *  n)  +  1))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  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
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  RepUR  ``rational-approx``  0
  THEN  (RWO    "int-rdiv-req"  0  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(2  *  n)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index