---

Step * 1 1 1 1 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(p)/r(4 * k)) < (r(-1)/r(2 * k))) ∨ ((r1/r(2 * k)) < (r(p)/r(4 * k)))
8. (r0 ≤ (r(p)/r(4 * k))) ∨ (↑isOdd(i))
⊢ ∃q:ℝ. ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
BY
{ ((Evaluate ⌜r
              = near-root(i;p;4 * k;2 * k)
              ∈ {r:ℤ × ℕ+| let a,b = r in (0 ≤ p ⇐⇒ 0 ≤ a) ∧ (|(r(a))/b^i - (r(p)/r(4 * k))| < (r1/r(2 * k)))} ⌝⋅
    THENA Auto
    )
   THEN Thin (-1)
   THEN D -1
   THEN D -2
   THEN Reduce (-1)
   THEN RenameVar `a' (-3)
   THEN RenameVar `b' (-2)
   THEN (With ⌜(r(a))/b⌝ (D 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(p)/r(4 * k)) < (r(-1)/r(2 * k))) ∨ ((r1/r(2 * k)) < (r(p)/r(4 * k)))
8. (r0 ≤ (r(p)/r(4 * k))) ∨ (↑isOdd(i))
9. a : ℤ
10. b : ℕ+
11. [%11] : (0 ≤ p ⇐⇒ 0 ≤ a) ∧ (|(r(a))/b^i - (r(p)/r(4 * k))| < (r1/r(2 * k)))
⊢ (|(r(a))/b^i - x| ≤ (r1/r(k)))
∧ ((r0 < (r(a))/b) ⇒ (r0 < x))
∧ (((r(a))/b < r0) ⇒ (x < r0))
∧ ((r0 < (r(a))/b) ∨ ((r(a))/b < r0) ∨ ((r(a))/b = r0))

---

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(p)/r(4  *  k))  <  (r(-1)/r(2  *  k)))  \mvee{}  ((r1/r(2  *  k))  <  (r(p)/r(4  *  k)))
8.  (r0  \mleq{}  (r(p)/r(4  *  k)))  \mvee{}  (\muparrow{}isOdd(i))
\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:
((Evaluate  \mkleeneopen{}r  =  near-root(i;p;4  *  k;2  *  k)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  D  -2
  THEN  Reduce  (-1)
  THEN  RenameVar  `a'  (-3)
  THEN  RenameVar  `b'  (-2)
  THEN  (With  \mkleeneopen{}(r(a))/b\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index