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


1. {2...}
2. {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. 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)))
6. lim n→∞.(λn.(q (n 1))) n^i x
7. ∀n,m:ℕ.
     (((r0 ≤ ((λn.(q (n 1))) n)) ∧ (r0 ≤ ((λn.(q (n 1))) m)))
     ∨ ((((λn.(q (n 1))) n) ≤ r0) ∧ (((λn.(q (n 1))) m) ≤ r0)))
8. ↑isEven(i)
9. : ℕ
⊢ r0 ≤ ((λn.(q (n 1))) m)
BY
TACTIC:(All Reduce
          THEN Auto
          THEN InstHyp [⌜1⌝(-5)⋅
          THEN Auto
          THEN RepeatFor ((D -1 THEN Auto))
          THEN Assert ⌜False⌝⋅
          THEN Auto
          THEN DVar `x'
          THEN Auto) }


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)))
4.  q  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}k:\mBbbN{}\msupplus{}
          ((|q  k\^{}i  -  x|  \mleq{}  (r1/r(k)))
          \mwedge{}  ((r0  <  (q  k))  {}\mRightarrow{}  (r0  <  x))
          \mwedge{}  (((q  k)  <  r0)  {}\mRightarrow{}  (x  <  r0))
          \mwedge{}  ((r0  <  (q  k))  \mvee{}  ((q  k)  <  r0)  \mvee{}  ((q  k)  =  r0)))
6.  lim  n\mrightarrow{}\minfty{}.(\mlambda{}n.(q  (n  +  1)))  n\^{}i  =  x
7.  \mforall{}n,m:\mBbbN{}.
          (((r0  \mleq{}  ((\mlambda{}n.(q  (n  +  1)))  n))  \mwedge{}  (r0  \mleq{}  ((\mlambda{}n.(q  (n  +  1)))  m)))
          \mvee{}  ((((\mlambda{}n.(q  (n  +  1)))  n)  \mleq{}  r0)  \mwedge{}  (((\mlambda{}n.(q  (n  +  1)))  m)  \mleq{}  r0)))
8.  \muparrow{}isEven(i)
9.  m  :  \mBbbN{}
\mvdash{}  r0  \mleq{}  ((\mlambda{}n.(q  (n  +  1)))  m)


By


Latex:
TACTIC:(All  Reduce
                THEN  Auto
                THEN  InstHyp  [\mkleeneopen{}m  +  1\mkleeneclose{}]  (-5)\mcdot{}
                THEN  Auto
                THEN  RepeatFor  2  ((D  -1  THEN  Auto))
                THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  DVar  `x'
                THEN  Auto)




Home Index