---

Step * of Lemma geometric-series-converges-ext

∀c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} . Σn.c^n = (r1/r1 - c)
BY
{ Extract of Obid: geometric-series-converges
  not unfolding  absval int-to-real rminus radd rmul rdiv mu mu-ge rlessw exp-ratio
  finishing with Auto
  normalizes to:
  
  λc,k. eval n = rlessw(r0;(r1 + -(c)) * (r1/r(k))) in
        eval x1 = rlessw(λn.|c n|;r1) in
          exp-ratio(|c x1| + (r1 x1);4 * x1;0;n + 1;1) }

---

Latex:

---

Latex:
\mforall{}c:\{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\}  .  \mSigma{}n.c\^{}n  =  (r1/r1  -  c)


By

---

Latex:
Extract  of  Obid:  geometric-series-converges
not  unfolding    absval  int-to-real  rminus  radd  rmul  rdiv  mu  mu-ge  rlessw  exp-ratio
finishing  with  Auto
normalizes  to:

\mlambda{}c,k.  eval  n  =  rlessw(r0;(r1  +  -(c))  *  (r1/r(k)))  in
            eval  x1  =  rlessw(\mlambda{}n.|c  n|;r1)  in
                exp-ratio(|c  x1|  +  (r1  x1);4  *  x1;0;n  +  1;1)

---

Home Index