---

Step * of Lemma rroot-exists1

∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} .
  ∃q:{q:ℕ ⟶ ℝ| 
      (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
      ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} 
   lim n→∞.q n^i = x
BY
{ (InstLemma `rroot-exists-part1` [] THEN RepeatFor 3 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .
    \mexists{}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))))\} 
      lim  n\mrightarrow{}\minfty{}.q  n\^{}i  =  x


By

---

Latex:
(InstLemma  `rroot-exists-part1`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto)

---

Home Index