---

Step * 1 2 of Lemma rpowers-converge


1. x : ℝ
2. (|x| < r1) ⇒ lim n→∞.x^n = r0
3. r1 < x
4. ∃e:ℝ. ((r0 < e) ∧ ((r1 + e) < x))
⊢ lim n →∞.x^n = ∞
BY
{ (ExRepD THEN InstLemma `rpower-greater-one` [⌜e⌝;⌜x⌝]⋅ THEN Auto)⋅ }

1
1. x : ℝ
2. (|x| < r1) ⇒ lim n→∞.x^n = r0
3. r1 < x
4. e : ℝ
5. r0 < e
6. (r1 + e) < x
7. ∀n:ℕ. (r1 + (r(n) * e)) < x^n supposing 1 < n
⊢ lim n →∞.x^n = ∞

---

Latex:

---

Latex:

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


By

---

Latex:
(ExRepD  THEN  InstLemma  `rpower-greater-one`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index