---

Step * 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. Σ{-1^i * x[i] | a≤i≤b} = Σ{r(-1)^i * x[i] | a≤i≤b}
⊢ |Σ{r(-1)^i * x[i] | a≤i≤b}| ≤ x[a]
BY
{ (Thin (-1)
   THEN Assert ⌜∀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)))))⌝⋅
   ) }

1
.....assertion..... 
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
⊢ ∀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)))))

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,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)))))
⊢ |Σ{r(-1)^i * x[i] | a≤i≤b}| ≤ x[a]

---

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.  \mSigma{}\{-1\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}  =  \mSigma{}\{r(-1)\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}
\mvdash{}  |\mSigma{}\{r(-1)\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}|  \mleq{}  x[a]


By

---

Latex:
(Thin  (-1)
  THEN  Assert  \mkleeneopen{}\mforall{}d,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)))))\mkleeneclose{}\mcdot{}
  )

---

Home Index