---

Step * 1 2 1 of Lemma rpowers-converge


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 = ∞
BY
{ ((D 0 THEN Auto) THEN UnfoldTopAb 0 THEN Assert ⌜∃N:ℕ. (1 < N ∧ ((r(k) - r1/e) < r(N)))⌝⋅) }

1
.....assertion..... 
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
8. k : ℕ+
⊢ ∃N:ℕ. (1 < N ∧ ((r(k) - r1/e) < r(N)))

2
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
8. k : ℕ+
9. ∃N:ℕ. (1 < N ∧ ((r(k) - r1/e) < r(N)))
⊢ ∃N:ℕ. ∀n:ℕ. ((N ≤ n) ⇒ (r(k) ≤ x^n))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  (|x|  <  r1)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x\^{}n  =  r0
3.  r1  <  x
4.  e  :  \mBbbR{}
5.  r0  <  e
6.  (r1  +  e)  <  x
7.  \mforall{}n:\mBbbN{}.  (r1  +  (r(n)  *  e))  <  x\^{}n  supposing  1  <  n
\mvdash{}  lim  n  \mrightarrow{}\minfty{}.x\^{}n  =  \minfty{}


By

---

Latex:
((D  0  THEN  Auto)  THEN  UnfoldTopAb  0  THEN  Assert  \mkleeneopen{}\mexists{}N:\mBbbN{}.  (1  <  N  \mwedge{}  ((r(k)  -  r1/e)  <  r(N)))\mkleeneclose{}\mcdot{})

---

Home Index