---

Step * 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
BY
{ (InstLemma `constant-rleq-limit` [⌜r0⌝;⌜λ2n.q n⌝;⌜y⌝]⋅ THEN Auto THEN DVar `q' THEN Unhide 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)
\mvdash{}  r0  \mleq{}  y


By

---

Latex:
(InstLemma  `constant-rleq-limit`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.q  n\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  DVar  `q'
  THEN  Unhide
  THEN  Auto)\mcdot{}

---

Home Index