Step
*
1
2
of Lemma
series-converges-tail2
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))
10. (Σ{x[i] | 0≤i≤n} - a + Σ{x[n] | 0≤n≤N - 1}) = (Σ{x[i + N] | 0≤i≤n - N} - a)
⊢ |Σ{x[i] | 0≤i≤n} - a + Σ{x[n] | 0≤n≤N - 1}| ≤ (r1/r(k))
BY
{ (RWO "-1" 0 THEN Auto) }
Latex:
Latex:
1. N : \mBbbN{}
2. x : \mBbbN{} {}\mrightarrow{} \mBbbR{}
3. a : \mBbbR{}
4. k : \mBbbN{}\msupplus{}
5. M : \mBbbN{}
6. \mforall{}n:\mBbbN{}. ((M \mleq{} n) {}\mRightarrow{} (|\mSigma{}\{x[i + N] | 0\mleq{}i\mleq{}n\} - a| \mleq{} (r1/r(k))))
7. n : \mBbbN{}
8. (N + M) \mleq{} n
9. |\mSigma{}\{x[i + N] | 0\mleq{}i\mleq{}n - N\} - a| \mleq{} (r1/r(k))
10. (\mSigma{}\{x[i] | 0\mleq{}i\mleq{}n\} - a + \mSigma{}\{x[n] | 0\mleq{}n\mleq{}N - 1\}) = (\mSigma{}\{x[i + N] | 0\mleq{}i\mleq{}n - N\} - a)
\mvdash{} |\mSigma{}\{x[i] | 0\mleq{}i\mleq{}n\} - a + \mSigma{}\{x[n] | 0\mleq{}n\mleq{}N - 1\}| \mleq{} (r1/r(k))
By
Latex:
(RWO "-1" 0 THEN Auto)
Home
Index