---

Step * 2 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)
⊢ y^i = x
BY
{ (InstLemma `unique-limit` [⌜λ2n.q n^i⌝;⌜y^i⌝;⌜x⌝]⋅
   THEN Auto
   THEN (GenConcl ⌜i = m ∈ ℕ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN FLemma `rmul-limit` [-5;-1]
   THEN Auto)⋅ }

1
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

---

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)
\mvdash{}  y\^{}i  =  x


By

---

Latex:
(InstLemma  `unique-limit`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.q  n\^{}i\mkleeneclose{};\mkleeneopen{}y\^{}i\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}i  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  FLemma  `rmul-limit`  [-5;-1]
  THEN  Auto)\mcdot{}

---

Home Index