---

Step * 1 1 2 2 1 of Lemma alternating-series-tail-bound


1. x : ℕ ⟶ ℝ
2. M : ℕ
3. ∀n:ℕ. ((M ≤ n) ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))
4. lim n→∞.x[n] = r0
5. a : {M...}
6. b : ℕ
7. a ≤ b
8. d : ℕ
9. ∀d:ℕd. ∀n,m:ℕ.
     ((a ≤ n)
     ⇒ ((m - n) ≤ d)
     ⇒ ((((-1)^n = 1 ∈ ℤ) ⇒ ((r0 ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ x[n])))
        ∧ (((-1)^n = (-1) ∈ ℤ) ⇒ ((-(x[n]) ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ r0)))))
10. n : ℕ
11. m : ℕ
12. a ≤ n
13. (m - n) ≤ d
14. n < m
⊢ (((-1)^n = 1 ∈ ℤ) ⇒ ((r0 ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ x[n])))
∧ (((-1)^n = (-1) ∈ ℤ) ⇒ ((-(x[n]) ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ r0)))
BY
{ ((RWO "rsum-split-first" 0 THENA Auto)⋅
   THEN (InstHyp [⌜d - 1⌝;⌜n + 1⌝;⌜m⌝] 9⋅ THENA Auto)
   THEN D -1
   THEN D 0
   THEN (D 0 THENA Auto)) }

1
1. x : ℕ ⟶ ℝ
2. M : ℕ
3. ∀n:ℕ. ((M ≤ n) ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))
4. lim n→∞.x[n] = r0
5. a : {M...}
6. b : ℕ
7. a ≤ b
8. d : ℕ
9. ∀d:ℕd. ∀n,m:ℕ.
     ((a ≤ n)
     ⇒ ((m - n) ≤ d)
     ⇒ ((((-1)^n = 1 ∈ ℤ) ⇒ ((r0 ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ x[n])))
        ∧ (((-1)^n = (-1) ∈ ℤ) ⇒ ((-(x[n]) ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ r0)))))
10. n : ℕ
11. m : ℕ
12. a ≤ n
13. (m - n) ≤ d
14. n < m
15. ((-1)^(n + 1) = 1 ∈ ℤ) ⇒ ((r0 ≤ Σ{r(-1)^i * x[i] | n + 1≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n + 1≤i≤m} ≤ x[n + 1]))
16. ((-1)^(n + 1) = (-1) ∈ ℤ) ⇒ ((-(x[n + 1]) ≤ Σ{r(-1)^i * x[i] | n + 1≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n + 1≤i≤m} ≤ r0))
17. (-1)^n = 1 ∈ ℤ
⊢ (r0 ≤ ((r(-1)^n * x[n]) + Σ{r(-1)^i * x[i] | n + 1≤i≤m}))
∧ (((r(-1)^n * x[n]) + Σ{r(-1)^i * x[i] | n + 1≤i≤m}) ≤ x[n])

2
1. x : ℕ ⟶ ℝ
2. M : ℕ
3. ∀n:ℕ. ((M ≤ n) ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))
4. lim n→∞.x[n] = r0
5. a : {M...}
6. b : ℕ
7. a ≤ b
8. d : ℕ
9. ∀d:ℕd. ∀n,m:ℕ.
     ((a ≤ n)
     ⇒ ((m - n) ≤ d)
     ⇒ ((((-1)^n = 1 ∈ ℤ) ⇒ ((r0 ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ x[n])))
        ∧ (((-1)^n = (-1) ∈ ℤ) ⇒ ((-(x[n]) ≤ Σ{r(-1)^i * x[i] | n≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n≤i≤m} ≤ r0)))))
10. n : ℕ
11. m : ℕ
12. a ≤ n
13. (m - n) ≤ d
14. n < m
15. ((-1)^(n + 1) = 1 ∈ ℤ) ⇒ ((r0 ≤ Σ{r(-1)^i * x[i] | n + 1≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n + 1≤i≤m} ≤ x[n + 1]))
16. ((-1)^(n + 1) = (-1) ∈ ℤ) ⇒ ((-(x[n + 1]) ≤ Σ{r(-1)^i * x[i] | n + 1≤i≤m}) ∧ (Σ{r(-1)^i * x[i] | n + 1≤i≤m} ≤ r0))
17. (-1)^n = (-1) ∈ ℤ
⊢ (-(x[n]) ≤ ((r(-1)^n * x[n]) + Σ{r(-1)^i * x[i] | n + 1≤i≤m}))
∧ (((r(-1)^n * x[n]) + Σ{r(-1)^i * x[i] | n + 1≤i≤m}) ≤ r0)

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  M  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}.  ((M  \mleq{}  n)  {}\mRightarrow{}  ((r0  \mleq{}  x[n])  \mwedge{}  (x[n  +  1]  \mleq{}  x[n])))
4.  lim  n\mrightarrow{}\minfty{}.x[n]  =  r0
5.  a  :  \{M...\}
6.  b  :  \mBbbN{}
7.  a  \mleq{}  b
8.  d  :  \mBbbN{}
9.  \mforall{}d:\mBbbN{}d.  \mforall{}n,m:\mBbbN{}.
          ((a  \mleq{}  n)
          {}\mRightarrow{}  ((m  -  n)  \mleq{}  d)
          {}\mRightarrow{}  ((((-1)\^{}n  =  1)  {}\mRightarrow{}  ((r0  \mleq{}  \mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\})  \mwedge{}  (\mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\}  \mleq{}  x[n])))
                \mwedge{}  (((-1)\^{}n  =  (-1))
                    {}\mRightarrow{}  ((-(x[n])  \mleq{}  \mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\})  \mwedge{}  (\mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\}  \mleq{}  r0)))))
10.  n  :  \mBbbN{}
11.  m  :  \mBbbN{}
12.  a  \mleq{}  n
13.  (m  -  n)  \mleq{}  d
14.  n  <  m
\mvdash{}  (((-1)\^{}n  =  1)  {}\mRightarrow{}  ((r0  \mleq{}  \mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\})  \mwedge{}  (\mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\}  \mleq{}  x[n])))
\mwedge{}  (((-1)\^{}n  =  (-1))  {}\mRightarrow{}  ((-(x[n])  \mleq{}  \mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\})  \mwedge{}  (\mSigma{}\{r(-1)\^{}i  *  x[i]  |  n\mleq{}i\mleq{}m\}  \mleq{}  r0)))


By

---

Latex:
((RWO  "rsum-split-first"  0  THENA  Auto)\mcdot{}
  THEN  (InstHyp  [\mkleeneopen{}d  -  1\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  9\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  D  0
  THEN  (D  0  THENA  Auto))

---

Home Index