---

Step * of Lemma rational-approx-property-alt

∀x:ℝ. ∀n:ℕ+.  (|(r(2 * n) * x) - r(x n)| ≤ r(2))
BY
{ (InstLemma `rational-approx-property` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (nRMul ⌜r(2 * n)⌝ (-1)⋅ THENA Auto)
   THEN (RWW  "rmul-nonneg-rabs" (-1) THENA Auto)
   THEN (RWO "-1<" 0 THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (|(r(2  *  n)  *  x)  -  r(x  n)|  \mleq{}  r(2))


By

---

Latex:
(InstLemma  `rational-approx-property`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (nRMul  \mkleeneopen{}r(2  *  n)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWW    "rmul-nonneg-rabs"  (-1)  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto))

---

Home Index