---

Step * of Lemma rational-approx-implies-req

∀[k:ℕ+]. ∀[x:ℝ]. ∀[a:ℕ+ ⟶ ℤ].
  ((∀n:ℕ+. (|x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)))) ⇒ {k-regular-seq(a) ∧ (accelerate(k;a) = x)})
BY
{ (Auto
   THEN Unfold `guard` 0
   THEN (Assert ∀n,m:ℕ+.  (|(r(a n)/r(2 * n)) - (r(a m)/r(2 * m))| ≤ ((r(k)/r(n)) + (r(k)/r(m)))) BY
               (Auto
                THEN (Assert |x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)) BY
                            Auto)
                THEN (Assert |x - (r(a m)/r(2 * m))| ≤ (r(k)/r(m)) BY
                            Auto)
                THEN UseTriangleInequality [⌜x⌝]⋅))) }

1
1. k : ℕ+
2. x : ℝ
3. a : ℕ+ ⟶ ℤ
4. ∀n:ℕ+. (|x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)))
5. ∀n,m:ℕ+.  (|(r(a n)/r(2 * n)) - (r(a m)/r(2 * m))| ≤ ((r(k)/r(n)) + (r(k)/r(m))))
⊢ k-regular-seq(a) ∧ (accelerate(k;a) = x)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbR{}].  \mforall{}[a:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    ((\mforall{}n:\mBbbN{}\msupplus{}.  (|x  -  (r(a  n)/r(2  *  n))|  \mleq{}  (r(k)/r(n))))  {}\mRightarrow{}  \{k-regular-seq(a)  \mwedge{}  (accelerate(k;a)  =  x)\})


By

---

Latex:
(Auto
  THEN  Unfold  `guard`  0
  THEN  (Assert  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(r(a  n)/r(2  *  n))  -  (r(a  m)/r(2  *  m))|  \mleq{}  ((r(k)/r(n))  +  (r(k)/r(m))))  BY
                          (Auto
                            THEN  (Assert  |x  -  (r(a  n)/r(2  *  n))|  \mleq{}  (r(k)/r(n))  BY
                                                    Auto)
                            THEN  (Assert  |x  -  (r(a  m)/r(2  *  m))|  \mleq{}  (r(k)/r(m))  BY
                                                    Auto)
                            THEN  UseTriangleInequality  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{})))

---

Home Index