---

Step * 1 2 of Lemma rroot-exists-part1


1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. ∀k:ℕ+
     ∃q:ℝ
      ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
⊢ ∃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
{ (Skolemize (-1) `q' THENA Auto) }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. ∀k:ℕ+
     ∃q:ℝ
      ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
4. q : k:ℕ+ ⟶ ℝ
5. ∀k:ℕ+
     ((|q k^i - x| ≤ (r1/r(k)))
     ∧ ((r0 < (q k)) ⇒ (r0 < x))
     ∧ (((q k) < r0) ⇒ (x < r0))
     ∧ ((r0 < (q k)) ∨ ((q k) < r0) ∨ ((q k) = r0)))
⊢ ∃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:

1.  i  :  \{2...\}
2.  x  :  \{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\} 
3.  \mforall{}k:\mBbbN{}\msupplus{}
          \mexists{}q:\mBbbR{}
            ((|q\^{}i  -  x|  \mleq{}  (r1/r(k)))
            \mwedge{}  ((r0  <  q)  {}\mRightarrow{}  (r0  <  x))
            \mwedge{}  ((q  <  r0)  {}\mRightarrow{}  (x  <  r0))
            \mwedge{}  ((r0  <  q)  \mvee{}  (q  <  r0)  \mvee{}  (q  =  r0)))
\mvdash{}  \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:
(Skolemize  (-1)  `q'  THENA  Auto)

---

Home Index