---

Step * of Lemma rroot-exists-part1

∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} .
  ∃q:ℕ ⟶ ℝ
   (lim n→∞.q n^i = x
   ∧ (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
   ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m)))))
BY
{ (Auto
   THEN (Evaluate ⌜xx = x ∈ {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} ⌝⋅ THENA (Auto THEN D 0 THEN With ⌜1⌝ (D 0)⋅ THEN Auto))
   THEN (RevHypSubst (-1) 0 THENA Auto)
   THEN Thin (-1)
   THEN Thin 2
   THEN RenameVar `x' (-1)) }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
⊢ ∃q:ℕ ⟶ ℝ
   (lim n→∞.q n^i = x
   ∧ (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
   ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m)))))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Evaluate  \mkleeneopen{}xx  =  x\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  D  0  THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  (RevHypSubst  (-1)  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  2
  THEN  RenameVar  `x'  (-1))

---

Home Index