---

Step * 1 1 1 1 1 1 of Lemma connectedness-main-lemma


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)))
9. ∀k:ℕ+. (blended-real(6 * k;x;g (c (6 * k))) = accelerate(3;x) ∈ (ℕ+k ⟶ ℤ))
10. n : ℕ+
11. [%10] : P accelerate(3;x) = P blended-real(6 * n;x;g (c (6 * n)))
⊢ ∃n@0:ℕ [(blended-real(6 * n;x;g (c (6 * n))) = (g n@0))]
BY
{ (D 0 With ⌜c (6 * n)⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|(g  n)  -  x|  \mleq{}  (r1/r(k)))))])
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)])
6.  c  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.    (((c  k)  \mleq{}  n)  {}\mRightarrow{}  (|(g  n)  -  x|  \mleq{}  (r1/r(k))))
8.  \mforall{}k:\mBbbN{}\msupplus{}.  (|x  -  g  (c  k)|  \mleq{}  (r1/r(k)))
9.  \mforall{}k:\mBbbN{}\msupplus{}.  (blended-real(6  *  k;x;g  (c  (6  *  k)))  =  accelerate(3;x))
10.  n  :  \mBbbN{}\msupplus{}
11.  [\%10]  :  P  accelerate(3;x)  =  P  blended-real(6  *  n;x;g  (c  (6  *  n)))
\mvdash{}  \mexists{}n@0:\mBbbN{}  [(blended-real(6  *  n;x;g  (c  (6  *  n)))  =  (g  n@0))]


By

---

Latex:
(D  0  With  \mkleeneopen{}c  (6  *  n)\mkleeneclose{}    THEN  Auto)

---

Home Index