---

Step * 1 1 1 2 1 of Lemma rroot-exists-part1


1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. k : ℕ+
4. p : ℤ
5. p = (x (2 * k)) ∈ ℤ
6. |x - (r(p)/r(4 * k))| ≤ (r1/r(2 * k))
7. ((r(-1)/r(2 * k)) ≤ (r(p)/r(4 * k))) ∧ ((r(p)/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)))
BY
{ (D (-1)
   THEN With ⌜r0⌝ (D 0)⋅
   THEN Auto
   THEN (RWO "rnexp-int" 0 THENA Auto)
   THEN (RWO "exp-zero" 0 THENA Auto)
   THEN (nRNorm 0 THENA Auto)
   THEN (RWO "rabs-rminus" 0 THENA Auto))⋅ }

1
1. i : {2...}
2. x : {x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} 
3. k : ℕ+
4. p : ℤ
5. p = (x (2 * k)) ∈ ℤ
6. |x - (r(p)/r(4 * k))| ≤ (r1/r(2 * k))
7. (r(-1)/r(2 * k)) ≤ (r(p)/r(4 * k))
8. (r(p)/r(4 * k)) ≤ (r1/r(2 * k))
⊢ |x| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\} 
3.  k  :  \mBbbN{}\msupplus{}
4.  p  :  \mBbbZ{}
5.  p  =  (x  (2  *  k))
6.  |x  -  (r(p)/r(4  *  k))|  \mleq{}  (r1/r(2  *  k))
7.  ((r(-1)/r(2  *  k))  \mleq{}  (r(p)/r(4  *  k)))  \mwedge{}  ((r(p)/r(4  *  k))  \mleq{}  (r1/r(2  *  k)))
\mvdash{}  \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:
(D  (-1)
  THEN  With  \mkleeneopen{}r0\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (RWO  "rnexp-int"  0  THENA  Auto)
  THEN  (RWO  "exp-zero"  0  THENA  Auto)
  THEN  (nRNorm  0  THENA  Auto)
  THEN  (RWO  "rabs-rminus"  0  THENA  Auto))\mcdot{}

---

Home Index