---

Step * of Lemma rnexp-converges

No Annotations
∀x:ℝ. ((|x| < r1) ⇒ lim n→∞.x^n = r0)
BY
{ (Auto
   THEN (InstLemma `rationals-dense-ext` [⌜|x|⌝;⌜r1⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert 0 ≤ m BY
               (SupposeNot
                THEN ((Assert r(m) ≤ r(-1) BY
                             Auto)
                      THEN nRMul ⌜r(n)⌝ (-4)⋅
                      THEN (Assert r0 ≤ |x| BY
                                  Auto)
                      THEN nRMul ⌜r(n)⌝ (-1)⋅
                      THEN (RW IntNormC (-1) THEN Auto)
                      THEN (Assert r0 ≤ r(-1) BY
                                  (RelRST THEN Auto))
                      THEN RWO "rleq-int" (-1)
                      THEN Auto)⋅
                ))) }

1
1. x : ℝ@i
2. |x| < r1
3. n : ℕ+
4. m : ℤ
5. |x| < (r(m)/r(n))
6. (r(m)/r(n)) < r1
7. 0 ≤ m
⊢ lim n→∞.x^n = r0

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbR{}.  ((|x|  <  r1)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x\^{}n  =  r0)


By

---

Latex:
(Auto
  THEN  (InstLemma  `rationals-dense-ext`  [\mkleeneopen{}|x|\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  0  \mleq{}  m  BY
                          (SupposeNot
                            THEN  ((Assert  r(m)  \mleq{}  r(-1)  BY
                                                      Auto)
                                        THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  (-4)\mcdot{}
                                        THEN  (Assert  r0  \mleq{}  |x|  BY
                                                                Auto)
                                        THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  (-1)\mcdot{}
                                        THEN  (RW  IntNormC  (-1)  THEN  Auto)
                                        THEN  (Assert  r0  \mleq{}  r(-1)  BY
                                                                (RelRST  THEN  Auto))
                                        THEN  RWO  "rleq-int"  (-1)
                                        THEN  Auto)\mcdot{}
                            )))

---

Home Index