---

Step * 1 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. m ≤ n
11. imax(N;M) ≤ n
12. imax(N;M) ≤ m
⊢ |Σ{-1^i * x[i] | m + 1≤i≤n}| ≤ (r1/r(k))
BY
{ ((Assert M ≤ imax(N;M) BY
          Auto)
   THEN (Assert N ≤ imax(N;M) BY
               Auto)
   THEN RWO "4" 0
   THEN Auto
   THEN (InstHyp [⌜m + 1⌝] 7⋅ THENA Auto)
   THEN (nRNorm (-1) THENA Auto)
   THEN RWO "rabs-of-nonneg" (-1)
   THEN Auto) }

---

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.  m  \mleq{}  n
11.  imax(N;M)  \mleq{}  n
12.  imax(N;M)  \mleq{}  m
\mvdash{}  |\mSigma{}\{-1\^{}i  *  x[i]  |  m  +  1\mleq{}i\mleq{}n\}|  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  M  \mleq{}  imax(N;M)  BY
                Auto)
  THEN  (Assert  N  \mleq{}  imax(N;M)  BY
                          Auto)
  THEN  RWO  "4"  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}m  +  1\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
  THEN  (nRNorm  (-1)  THENA  Auto)
  THEN  RWO  "rabs-of-nonneg"  (-1)
  THEN  Auto)

---

Home Index