Step
*
1
2
1
3
of Lemma
rroot-exists-part1
1. i : {2...}
2. x : {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. q : 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. m : ℕ
⊢ r0 ≤ ((λn.(q (n + 1))) m)
BY
{ TACTIC:(All Reduce
          THEN Auto
          THEN InstHyp [⌜m + 1⌝] (-5)⋅
          THEN Auto
          THEN RepeatFor 2 ((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