---

Step * of Lemma rroot-exists-part2

∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} . ∀q:{q:ℕ ⟶ ℝ| 
                                                   (∀n,m:ℕ.
                                                      (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
                                                   ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} .
  (lim n→∞.q n^i = x ⇒ cauchy(n.q n))
BY
{ (Auto
   THEN Unfold `converges-to` -1
   THEN Skolemize (-1) `h'
   THEN Auto
   THEN Thin (-3)
   THEN D 0
   THEN Auto
   THEN (Assert k^i ∈ ℕ+ BY
               Auto)
   THEN (Assert 2 * k^i ∈ ℕ+ BY
               Auto)) }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. q : {q:ℕ ⟶ ℝ| 
        (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
        ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} 
4. h : k:ℕ+ ⟶ ℕ
5. ∀k:ℕ+. ∀n:ℕ.  (((h k) ≤ n) ⇒ (|q n^i - x| ≤ (r1/r(k))))
6. k : ℕ+
7. k^i ∈ ℕ+
8. 2 * k^i ∈ ℕ+
⊢ ∃N:{ℕ| (∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|(q n) - q m| ≤ (r1/r(k)))))}

---

Latex:

---

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .  \mforall{}q:\{q:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}| 
                                                                                                      (\mforall{}n,m:\mBbbN{}.
                                                                                                            (((r0  \mleq{}  (q  n))  \mwedge{}  (r0  \mleq{}  (q  m)))
                                                                                                            \mvee{}  (((q  n)  \mleq{}  r0)  \mwedge{}  ((q  m)  \mleq{}  r0))))
                                                                                                      \mwedge{}  ((\muparrow{}isEven(i))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  (r0  \mleq{}  (q  m))))\}  .
    (lim  n\mrightarrow{}\minfty{}.q  n\^{}i  =  x  {}\mRightarrow{}  cauchy(n.q  n))


By

---

Latex:
(Auto
  THEN  Unfold  `converges-to`  -1
  THEN  Skolemize  (-1)  `h'
  THEN  Auto
  THEN  Thin  (-3)
  THEN  D  0
  THEN  Auto
  THEN  (Assert  k\^{}i  \mmember{}  \mBbbN{}\msupplus{}  BY
                          Auto)
  THEN  (Assert  2  *  k\^{}i  \mmember{}  \mBbbN{}\msupplus{}  BY
                          Auto))

---

Home Index