---

Step * of Lemma rpowers-converge-ext

∀x:ℝ. (((|x| < r1) ⇒ lim n→∞.x^n = r0) ∧ ((r1 < x) ⇒ lim n →∞.x^n = ∞))
BY
{ Extract of Obid: rpowers-converge
  not unfolding  divide absval rlessw rdiv radd rmul exp-ratio mu
  finishing with (Reduce 0 THEN Auto)
  normalizes to:
  
  λx.<λ%.eval x1 = rlessw(λn.|x n|;λk.(2 * k * 1)) in
         λk.exp-ratio(|x x1| + (2 * x1 * 1);4 * x1;0;k;1)
     , λ%,k. <((||((λk@0.(2 * k@0 * k)) + (λn.(-(2 * n * 1)))/(x + (λn.(-(2 * n * 1)))/λk.(2 * k * 2))) 1|| + 4) ÷ 2)
              + 1
             , λn,%15,n. <λv.Ax, Ax, Ax>
             >
     > }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (((|x|  <  r1)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x\^{}n  =  r0)  \mwedge{}  ((r1  <  x)  {}\mRightarrow{}  lim  n  \mrightarrow{}\minfty{}.x\^{}n  =  \minfty{}))


By

---

Latex:
Extract  of  Obid:  rpowers-converge
not  unfolding    divide  absval  rlessw  rdiv  radd  rmul  exp-ratio  mu
finishing  with  (Reduce  0  THEN  Auto)
normalizes  to:

\mlambda{}x.<\mlambda{}\%.eval  x1  =  rlessw(\mlambda{}n.|x  n|;\mlambda{}k.(2  *  k  *  1))  in
              \mlambda{}k.exp-ratio(|x  x1|  +  (2  *  x1  *  1);4  *  x1;0;k;1)
      ,  \mlambda{}\%,k.  <((||((\mlambda{}k@0.(2  *  k@0  *  k))  +  (\mlambda{}n.(-(2  *  n  *  1)))/(x
                                +  (\mlambda{}n.(-(2  *  n  *  1)))/\mlambda{}k.(2  *  k  *  2))) 
                                1||
                        +  4)  \mdiv{}  2)
                        +  1
                      ,  \mlambda{}n,\%15,n.  <\mlambda{}v.Ax,  Ax,  Ax>
                      >
      >

---

Home Index