---

Step * 1 1 of Lemma alternating-series-converges


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))
BY
{ ((Assert ⌜∀n,m:ℕ.
              ((m ≤ n)
              ⇒ (imax(N;M) ≤ n)
              ⇒ (imax(N;M) ≤ m)
              ⇒ (|Σ{-1^i * x[i] | 0≤i≤n} - Σ{-1^i * x[i] | 0≤i≤m}| ≤ (r1/r(k))))⌝⋅
   THENM ((Decide ⌜n ≤ m⌝⋅ THENA Auto)
          THENL [((RWO "rabs-difference-symmetry" 0⋅ THENA Auto) THEN BHyp -2 THEN Auto); (BHyp -2 THEN Auto)]
         )
   )
   THEN RepeatFor 4 (Thin (-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. m ≤ n
11. imax(N;M) ≤ n
12. imax(N;M) ≤ m
⊢ |Σ{-1^i * x[i] | m + 1≤i≤n}| ≤ (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.  \mforall{}a:\{M  +  1...\}.  \mforall{}b:\mBbbN{}.    (|\mSigma{}\{-1\^{}i  *  x[i]  |  a\mleq{}i\mleq{}b\}|  \mleq{}  x[a])
5.  k  :  \mBbbN{}\msupplus{}
6.  N  :  \mBbbN{}
7.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|x[n]  -  r0|  \mleq{}  (r1/r(k))))
8.  n  :  \mBbbN{}
9.  m  :  \mBbbN{}
10.  imax(N;M)  \mleq{}  n
11.  imax(N;M)  \mleq{}  m
\mvdash{}  |\mSigma{}\{-1\^{}i  *  x[i]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{-1\^{}i  *  x[i]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}n,m:\mBbbN{}.
                        ((m  \mleq{}  n)
                        {}\mRightarrow{}  (imax(N;M)  \mleq{}  n)
                        {}\mRightarrow{}  (imax(N;M)  \mleq{}  m)
                        {}\mRightarrow{}  (|\mSigma{}\{-1\^{}i  *  x[i]  |  0\mleq{}i\mleq{}n\}  -  \mSigma{}\{-1\^{}i  *  x[i]  |  0\mleq{}i\mleq{}m\}|  \mleq{}  (r1/r(k))))\mkleeneclose{}\mcdot{}
  THENM  ((Decide  \mkleeneopen{}n  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
                THENL  [((RWO  "rabs-difference-symmetry"  0\mcdot{}  THENA  Auto)  THEN  BHyp  -2  THEN  Auto)
                            ;  (BHyp  -2  THEN  Auto)]
              )
  )
  THEN  RepeatFor  4  (Thin  (-1))
  THEN  Auto
  THEN  RWO  "rsum-difference"  0
  THEN  Auto)

---

Home Index