---

Step * 2 1 of Lemma rroot-exists


1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. q : {q:ℕ ⟶ ℝ| 
        (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
        ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} 
4. lim n→∞.q n^i = x
5. y : ℝ
6. lim n→∞.q n = y
7. (↑isEven(i)) ⇒ (r0 ≤ y)
8. m : ℤ
9. [%7] : 0 < m
10. lim n→∞.q n^m - 1 = y^m - 1
11. lim n→∞.(q n) * q n^m - 1 = y * y^m - 1
⊢ lim n→∞.q n^m = y^m
BY
{ (MoveToConcl (-1)
   THEN BLemma `converges-to_functionality`
   THEN Auto
   THEN ((RW (AddrC [2] (LemmaC `rnexp_unroll`)) 0 THENA Auto)
         THEN RepeatFor 2 (AutoSplit)
         THEN nRNorm 0
         THEN Auto
         THEN HypSubst' (-1) 0
         THEN Reduce 0
         THEN nRNorm 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\} 
3.  q  :  \{q:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}| 
                (\mforall{}n,m:\mBbbN{}.    (((r0  \mleq{}  (q  n))  \mwedge{}  (r0  \mleq{}  (q  m)))  \mvee{}  (((q  n)  \mleq{}  r0)  \mwedge{}  ((q  m)  \mleq{}  r0))))
                \mwedge{}  ((\muparrow{}isEven(i))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  (r0  \mleq{}  (q  m))))\} 
4.  lim  n\mrightarrow{}\minfty{}.q  n\^{}i  =  x
5.  y  :  \mBbbR{}
6.  lim  n\mrightarrow{}\minfty{}.q  n  =  y
7.  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  y)
8.  m  :  \mBbbZ{}
9.  [\%7]  :  0  <  m
10.  lim  n\mrightarrow{}\minfty{}.q  n\^{}m  -  1  =  y\^{}m  -  1
11.  lim  n\mrightarrow{}\minfty{}.(q  n)  *  q  n\^{}m  -  1  =  y  *  y\^{}m  -  1
\mvdash{}  lim  n\mrightarrow{}\minfty{}.q  n\^{}m  =  y\^{}m


By

---

Latex:
(MoveToConcl  (-1)
  THEN  BLemma  `converges-to\_functionality`
  THEN  Auto
  THEN  ((RW  (AddrC  [2]  (LemmaC  `rnexp\_unroll`))  0  THENA  Auto)
              THEN  RepeatFor  2  (AutoSplit)
              THEN  nRNorm  0
              THEN  Auto
              THEN  HypSubst'  (-1)  0
              THEN  Reduce  0
              THEN  nRNorm  0
              THEN  Auto)\mcdot{})

---

Home Index