---

Step * 1 of Lemma alternating-series-converges


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 + 1...}. ∀b:ℕ.  (|Σ{-1^i * x[i] | a≤i≤b}| ≤ x[a])
⊢ Σn.-1^n * x[n]↓
BY
{ (RepUR ``series-converges series-sum`` 0
   THEN Fold `converges` 0
   THEN RWO "converges-iff-cauchy-ext" 0
   THEN Try (Complete (Auto))
   THEN D 0
   THEN Auto
   THEN (With ⌜k⌝ (D (-3))⋅ THENA Auto)
   THEN (D -1 THEN ExRepD)
   THEN UseWitness ⌜imax(N;M)⌝⋅
   THEN MemTypeCD
   THEN Auto
   THEN Try (Complete ((Unfold `imax` 0 THEN AutoSplit)))
   THEN skip{((((Decide ⌜n ≤ m⌝⋅ THENA Auto)
                THENL [(RenameTo `a' `n'
                        THEN RenameTo `b' `m'
                        THEN PromoteHyp (-4) (-5)
                        THEN PromoteHyp (-2) (-3)⋅
                        THEN (RWO "rabs-difference-symmetry" 0⋅ THENA Auto))
                      ; ((Assert ⌜m ≤ n⌝⋅ THENA Auto) THEN Thin (-2) THEN RenameTo `b' `n' THEN RenameTo `a' `m')]
               )⋅
               THEN RenameVar `%b' (-3)
               THEN RenameVar `%a' (-2)
               THEN RenameVar `%c' (-1))
              THEN Auto
              THEN RWO "rsum-difference" 0
              THEN Auto)}) }

1
1. x : ℕ ⟶ ℝ
2. M : ℕ
3. ∀n:ℕ. (M < n ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))
4. ∀a:{M + 1...}. ∀b:ℕ.  (|Σ{-1^i * x[i] | a≤i≤b}| ≤ x[a])
5. k : ℕ+
6. N : ℕ
7. ∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - r0| ≤ (r1/r(k))))
8. n : ℕ
9. m : ℕ
10. imax(N;M) ≤ n
11. imax(N;M) ≤ m
⊢ |Σ{-1^i * x[i] | 0≤i≤n} - Σ{-1^i * x[i] | 0≤i≤m}| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  M  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}.  (M  <  n  {}\mRightarrow{}  ((r0  \mleq{}  x[n])  \mwedge{}  (x[n  +  1]  \mleq{}  x[n])))
4.  lim  n\mrightarrow{}\minfty{}.x[n]  =  r0
5.  \mforall{}a:\{M  +  1...\}.  \mforall{}b:\mBbbN{}.    (|\mSigma{}\{-1\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}|  \mleq{}  x[a])
\mvdash{}  \mSigma{}n.-1\^{}n  *  x[n]\mdownarrow{}


By

---

Latex:
(RepUR  ``series-converges  series-sum``  0
  THEN  Fold  `converges`  0
  THEN  RWO  "converges-iff-cauchy-ext"  0
  THEN  Try  (Complete  (Auto))
  THEN  D  0
  THEN  Auto
  THEN  (With  \mkleeneopen{}k\mkleeneclose{}  (D  (-3))\mcdot{}  THENA  Auto)
  THEN  (D  -1  THEN  ExRepD)
  THEN  UseWitness  \mkleeneopen{}imax(N;M)\mkleeneclose{}\mcdot{}
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  (Complete  ((Unfold  `imax`  0  THEN  AutoSplit)))
  THEN  skip\{((((Decide  \mkleeneopen{}n  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THENL  [(RenameTo  `a'  `n'
                                            THEN  RenameTo  `b'  `m'
                                            THEN  PromoteHyp  (-4)  (-5)
                                            THEN  PromoteHyp  (-2)  (-3)\mcdot{}
                                            THEN  (RWO  "rabs-difference-symmetry"  0\mcdot{}  THENA  Auto))
                                        ;  ((Assert  \mkleeneopen{}m  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                                              THEN  Thin  (-2)
                                              THEN  RenameTo  `b'  `n'
                                              THEN  RenameTo  `a'  `m')]
                          )\mcdot{}
                          THEN  RenameVar  `\%b'  (-3)
                          THEN  RenameVar  `\%a'  (-2)
                          THEN  RenameVar  `\%c'  (-1))
                        THEN  Auto
                        THEN  RWO  "rsum-difference"  0
                        THEN  Auto)\})

---

Home Index