---

Step * of Lemma series-converges-tail2

No Annotations
∀N:ℕ. ∀x:ℕ ⟶ ℝ.  (Σn.x[n + N]↓ ⇒ Σn.x[n]↓)
BY
{ (Auto
   THEN D -1
   THEN (With ⌜a + Σ{x[n] | 0≤n≤N - 1}⌝ (D 0)⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN D -1
   THEN RenameVar `M' (-2)
   THEN With ⌜N + M⌝ (D 0)⋅
   THEN Auto
   THEN (InstHyp [⌜n - N⌝] (-3)⋅ THENA Auto)) }

1
1. N : ℕ
2. x : ℕ ⟶ ℝ
3. a : ℝ
4. k : ℕ+
5. M : ℕ
6. ∀n:ℕ. ((M ≤ n) ⇒ (|Σ{x[i + N] | 0≤i≤n} - a| ≤ (r1/r(k))))
7. n : ℕ
8. (N + M) ≤ n
9. |Σ{x[i + N] | 0≤i≤n - N} - a| ≤ (r1/r(k))
⊢ |Σ{x[i] | 0≤i≤n} - a + Σ{x[n] | 0≤n≤N - 1}| ≤ (r1/r(k))

---

Latex:

---

Latex:
No  Annotations
\mforall{}N:\mBbbN{}.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.    (\mSigma{}n.x[n  +  N]\mdownarrow{}  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{})


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (With  \mkleeneopen{}a  +  \mSigma{}\{x[n]  |  0\mleq{}n\mleq{}N  -  1\}\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  D  -1
  THEN  RenameVar  `M'  (-2)
  THEN  With  \mkleeneopen{}N  +  M\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}n  -  N\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))

---

Home Index