---

Step * of Lemma series-converges-tail

∀x:ℕ ⟶ ℝ. (Σn.x[n]↓ ⇒ (∀y:ℕ ⟶ ℝ. ((∃N:ℕ. ∀n:{N...}. (y[n] = x[n])) ⇒ Σn.y[n]↓)))
BY
{ ((Auto THEN D -1 THEN D 2 THEN With ⌜a + Σ{y[n] - x[n] | 0≤n≤N}⌝ (D 0)⋅)
   THEN Auto
   THEN RepeatFor 3 (ParallelOp 3)
   THEN D (-1)⋅
   THEN (With ⌜imax(N;N1)⌝ (D 0)⋅ THENA Auto)
   THEN (RepeatFor 2 (ParallelLast) THENA (RWO  "-1<" 0 THEN Auto))) }

1
1. x : ℕ ⟶ ℝ
2. a : ℝ
3. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|Σ{x[i] | 0≤i≤n} - a| ≤ (r1/r(k)))))})
4. y : ℕ ⟶ ℝ
5. N : ℕ
6. ∀n:{N...}. (y[n] = x[n])
7. k : ℕ+
8. N1 : ℕ
9. ∀n:ℕ. ((N1 ≤ n) ⇒ (|Σ{x[i] | 0≤i≤n} - a| ≤ (r1/r(k))))
10. n : ℕ
11. imax(N;N1) ≤ n
12. |Σ{x[i] | 0≤i≤n} - a| ≤ (r1/r(k))
⊢ |Σ{y[i] | 0≤i≤n} - a + Σ{y[n] - x[n] | 0≤n≤N}| ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  (\mSigma{}n.x[n]\mdownarrow{}  {}\mRightarrow{}  (\mforall{}y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  ((\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  (y[n]  =  x[n]))  {}\mRightarrow{}  \mSigma{}n.y[n]\mdownarrow{})))


By

---

Latex:
((Auto  THEN  D  -1  THEN  D  2  THEN  With  \mkleeneopen{}a  +  \mSigma{}\{y[n]  -  x[n]  |  0\mleq{}n\mleq{}N\}\mkleeneclose{}  (D  0)\mcdot{})
  THEN  Auto
  THEN  RepeatFor  3  (ParallelOp  3)
  THEN  D  (-1)\mcdot{}
  THEN  (With  \mkleeneopen{}imax(N;N1)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  (RepeatFor  2  (ParallelLast)  THENA  (RWO    "-1<"  0  THEN  Auto)))

---

Home Index