---

Step * 1 of Lemma connectedness-main-lemma


1. x : ℝ
2. g : ℕ ⟶ ℝ
3. lim n→∞.g n = x
4. P : ℝ ⟶ 𝔹
5. ∀G:n:ℕ+ ⟶ {y:ℝ| accelerate(3;x) = y ∈ (ℕ+n ⟶ ℤ)} . (∃n:ℕ+ [P accelerate(3;x) = P (G n)])
⊢ ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:ℕ [(z = (g n))])
BY
{ (Unfold `converges-to` -3
   THEN (Skolemize  (-3) `c' THENA Auto)
   THEN (Assert ∀k:ℕ+. (|x - g (c k)| ≤ (r1/r(k))) BY
               (ParallelLast THEN Auto THEN RWO  "rabs-difference-symmetry" 0 THEN Auto))) }

1
1. x : ℝ
2. g : ℕ ⟶ ℝ
3. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|(g n) - x| ≤ (r1/r(k)))))])
4. P : ℝ ⟶ 𝔹
5. ∀G:n:ℕ+ ⟶ {y:ℝ| accelerate(3;x) = y ∈ (ℕ+n ⟶ ℤ)} . (∃n:ℕ+ [P accelerate(3;x) = P (G n)])
6. c : k:ℕ+ ⟶ ℕ
7. ∀k:ℕ+. ∀n:ℕ.  (((c k) ≤ n) ⇒ (|(g n) - x| ≤ (r1/r(k))))
8. ∀k:ℕ+. (|x - g (c k)| ≤ (r1/r(k)))
⊢ ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:ℕ [(z = (g n))])

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  lim  n\mrightarrow{}\minfty{}.g  n  =  x
4.  P  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  accelerate(3;x)  =  y\}  .  (\mexists{}n:\mBbbN{}\msupplus{}  [P  accelerate(3;x)  =  P  (G  n)])
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  P  z  =  P  accelerate(3;x)\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (g  n))])


By

---

Latex:
(Unfold  `converges-to`  -3
  THEN  (Skolemize    (-3)  `c'  THENA  Auto)
  THEN  (Assert  \mforall{}k:\mBbbN{}\msupplus{}.  (|x  -  g  (c  k)|  \mleq{}  (r1/r(k)))  BY
                          (ParallelLast  THEN  Auto  THEN  RWO    "rabs-difference-symmetry"  0  THEN  Auto)))

---

Home Index