---

Step * of Lemma rpowers-converge

∀x:ℝ. (((|x| < r1) ⇒ lim n→∞.x^n = r0) ∧ ((r1 < x) ⇒ lim n →∞.x^n = ∞))
BY
{ (Auto THEN Try ((BLemma `rnexp-converges` THEN Auto))) }

1
1. x : ℝ
2. (|x| < r1) ⇒ lim n→∞.x^n = r0
3. r1 < x
⊢ lim n →∞.x^n = ∞

---

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:
(Auto  THEN  Try  ((BLemma  `rnexp-converges`  THEN  Auto)))

---

Home Index