---

Step * 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)))
⊢ ∃q:ℝ. ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = r0)))
BY
{ (Assert (r0 ≤ (r(p)/r(4 * k))) ∨ (↑isOdd(i)) BY
         (( Decide ⌜0 ≤ p⌝⋅ THENA Auto)
          THEN Try ((OrLeft THEN Complete (Auto)))
          THEN ((InstLemma `odd-or-even` [⌜i⌝]⋅ THENA Auto)
                THEN (RW assert_pushdownC (-1) THENA Auto)
                THEN D -1
                THEN Auto
                THEN (Assert ⌜False⌝⋅
                      THEN Auto
                      THEN DVar `x'
                      THEN ThinTrivial
                      THEN RWO "rabs-difference-bound-rleq" (-5)⋅
                      THEN Auto
                      THEN (Assert p ≤ (-1) BY
                                  Auto')
                      THEN Thin (-4)
                      THEN Mul ⌜4 * k⌝ (-1)⋅
                      THEN (D (-5) THEN Try (Complete ((AllHyps (RWO "rless-int-fractions") THEN Auto)⋅)))
                      THEN nRAdd ⌜(r1/r(2 * k))⌝ (-5)⋅
                      THEN Auto
                      THEN (RWW "radd-rdiv radd-int" (-5) THENA Auto)
                      THEN Reduce (-5)
                      THEN nRNorm (-5)
                      THEN Auto
                      THEN nRNorm (-6)
                      THEN 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))
⊢ ∃q:ℝ. ((|q^i - x| ≤ (r1/r(k))) ∧ ((r0 < q) ⇒ (r0 < x)) ∧ ((q < r0) ⇒ (x < r0)) ∧ ((r0 < q) ∨ (q < r0) ∨ (q = 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)))
\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:
(Assert  (r0  \mleq{}  (r(p)/r(4  *  k)))  \mvee{}  (\muparrow{}isOdd(i))  BY
              ((  Decide  \mkleeneopen{}0  \mleq{}  p\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Try  ((OrLeft  THEN  Complete  (Auto)))
                THEN  ((InstLemma  `odd-or-even`  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
                            THEN  D  -1
                            THEN  Auto
                            THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                                        THEN  Auto
                                        THEN  DVar  `x'
                                        THEN  ThinTrivial
                                        THEN  RWO  "rabs-difference-bound-rleq"  (-5)\mcdot{}
                                        THEN  Auto
                                        THEN  (Assert  p  \mleq{}  (-1)  BY
                                                                Auto')
                                        THEN  Thin  (-4)
                                        THEN  Mul  \mkleeneopen{}4  *  k\mkleeneclose{}  (-1)\mcdot{}
                                        THEN  (D  (-5)
                                                    THEN  Try  (Complete  ((AllHyps  (RWO  "rless-int-fractions")  THEN  Auto)\mcdot{}))
                                                    )
                                        THEN  nRAdd  \mkleeneopen{}(r1/r(2  *  k))\mkleeneclose{}  (-5)\mcdot{}
                                        THEN  Auto
                                        THEN  (RWW  "radd-rdiv  radd-int"  (-5)  THENA  Auto)
                                        THEN  Reduce  (-5)
                                        THEN  nRNorm  (-5)
                                        THEN  Auto
                                        THEN  nRNorm  (-6)
                                        THEN  Auto)\mcdot{})\mcdot{}))\mcdot{}

---

Home Index