---

Step * 1 2 1 2 1 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
8. k : ℕ+
9. N : ℕ
10. 1 < N
11. (r(k) - r1/e) < r(N)
12. n : ℕ
13. N ≤ n
14. (r1 + (r(n) * e)) < x^n
⊢ r(k) ≤ x^n
BY
{ ((Assert r(N) ≤ r(n) BY
          Auto)
   THEN ((nRMul ⌜e⌝ (-1))⋅ THENA Auto)
   THEN ((nRAdd ⌜r1⌝ (-1))⋅ THENA Auto)
   THEN OnMaybeHyp 11 (\h. ((nRMul ⌜e⌝ h)⋅ THEN Auto THEN (nRAdd ⌜r1⌝ h)⋅ THEN RW IntNormC h THEN Auto)))⋅ }

---

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
8.  k  :  \mBbbN{}\msupplus{}
9.  N  :  \mBbbN{}
10.  1  <  N
11.  (r(k)  -  r1/e)  <  r(N)
12.  n  :  \mBbbN{}
13.  N  \mleq{}  n
14.  (r1  +  (r(n)  *  e))  <  x\^{}n
\mvdash{}  r(k)  \mleq{}  x\^{}n


By

---

Latex:
((Assert  r(N)  \mleq{}  r(n)  BY
                Auto)
  THEN  ((nRMul  \mkleeneopen{}e\mkleeneclose{}  (-1))\mcdot{}  THENA  Auto)
  THEN  ((nRAdd  \mkleeneopen{}r1\mkleeneclose{}  (-1))\mcdot{}  THENA  Auto)
  THEN  OnMaybeHyp  11  (\mbackslash{}h.  ((nRMul  \mkleeneopen{}e\mkleeneclose{}  h)\mcdot{}
                                                    THEN  Auto
                                                    THEN  (nRAdd  \mkleeneopen{}r1\mkleeneclose{}  h)\mcdot{}
                                                    THEN  RW  IntNormC  h
                                                    THEN  Auto)))\mcdot{}

---

Home Index