---

Step * of Lemma alternating-series-converges-ext

∀x:ℕ ⟶ ℝ. ((∃M:ℕ. ∀n:ℕ. (M < n ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))) ⇒ lim n→∞.x[n] = r0 ⇒ Σn.-1^n * x[n]↓)
BY
{ Extract of Obid: alternating-series-converges
  not unfolding  divide rational-approx canonical-bound rsum rmul rabs rnexp imax fastexp
  finishing with Auto
  normalizes to:
  
  λx,Mp,cnvg. let M,_ = Mp 
              in <λn.eval m = 4 * n in
                     (Σ{eval k = -1^i in
                        λn.if (k) < (0)
                              then -(x i ((-k) * n))
                              else if (0) < (k)  then x i (k * n)  else 0 | 0≤i≤imax(cnvg m;M)} 
                      m) ÷ 4
                 , λk.(imax(cnvg (4 * k);M) + 1)
                 > }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
    ((\mexists{}M:\mBbbN{}.  \mforall{}n:\mBbbN{}.  (M  <  n  {}\mRightarrow{}  ((r0  \mleq{}  x[n])  \mwedge{}  (x[n  +  1]  \mleq{}  x[n]))))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  r0
    {}\mRightarrow{}  \mSigma{}n.-1\^{}n  *  x[n]\mdownarrow{})


By

---

Latex:
Extract  of  Obid:  alternating-series-converges
not  unfolding    divide  rational-approx  canonical-bound  rsum  rmul  rabs  rnexp  imax  fastexp
finishing  with  Auto
normalizes  to:

\mlambda{}x,Mp,cnvg.  let  M,$_{}$  =  Mp 
                        in  <\mlambda{}n.eval  m  =  4  *  n  in
                                      (\mSigma{}\{eval  k  =  -1\^{}i  in
                                            \mlambda{}n.if  (k)  <  (0)
                                                        then  -(x  i  ((-k)  *  n))
                                                        else  if  (0)  <  (k)    then  x  i  (k  *  n)    else  0  |  0\mleq{}i\mleq{}imax(cnvg  m;M)\} 
                                        m)  \mdiv{}  4
                              ,  \mlambda{}k.(imax(cnvg  (4  *  k);M)  +  1)
                              >

---

Home Index