---

Step * 1 1 of Lemma rpowers-converge

.....assertion..... 
1. x : ℝ
2. (|x| < r1) ⇒ lim n→∞.x^n = r0
3. r1 < x
⊢ ∃e:ℝ. ((r0 < e) ∧ ((r1 + e) < x))
BY
{ ((InstConcl [ ⌜(x - r1/r(2))⌝]⋅ THEN Auto) THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbR{}
2.  (|x|  <  r1)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x\^{}n  =  r0
3.  r1  <  x
\mvdash{}  \mexists{}e:\mBbbR{}.  ((r0  <  e)  \mwedge{}  ((r1  +  e)  <  x))


By

---

Latex:
((InstConcl  [  \mkleeneopen{}(x  -  r1/r(2))\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index