---

Step * 1 1 of Lemma rroot-exists-part1

.....assertion..... 
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
⊢ ∀k:ℕ+
    ∃q:ℝ. ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
BY
{ (Auto
   THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜2 * k⌝]⋅ THENA Auto)
   THEN RepUR ``rational-approx`` -1
   THEN (RW IntNormC (-1) THENA Auto)
   THEN (RWO "int-rdiv-req" (-1) THENA Auto))⋅ }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. k : ℕ+
4. |x - (r(x (2 * k))/r(4 * k))| ≤ (r1/r(2 * k))
⊢ ∃q:ℝ. ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))

---

Latex:

---

Latex:
.....assertion..... 
1.  i  :  \{2...\}
2.  x  :  \{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\} 
\mvdash{}  \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)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}2  *  k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``rational-approx``  -1
  THEN  (RW  IntNormC  (-1)  THENA  Auto)
  THEN  (RWO  "int-rdiv-req"  (-1)  THENA  Auto))\mcdot{}

---

Home Index