---

Step * of Lemma rroot-exists1-ext

No Annotations
∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} .
  ∃q:{q:ℕ ⟶ ℝ| 
      (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))
      ∧ ((↑isEven(i)) ⇒ (∀m:ℕ. (r0 ≤ (q m))))} 
   lim n→∞.q n^i = x
BY
{ Extract of Obid: rroot-exists1
  not unfolding  divide near-root rlessw mu-ge absval
  finishing with Auto
  normalizes to:
  
  λi,x. eval xx = x in
        <λn.eval p = xx (2 * (n + 1)) in
            if (1 * 4 * (n + 1)) < (p * 2 * (n + 1))
               then if (p * 2 * (n + 1)) < ((-1) * 4 * (n + 1))
                       then eval r = near-root(i;p;4 * (n + 1);2 * (n + 1)) in
                            let r1,r2 = r 
                            in eval k = r2 in
                               λn.((2 * n * r1) ÷ k)
                       else eval r = near-root(i;p;4 * (n + 1);2 * (n + 1)) in
                            let r1,r2 = r 
                            in eval k = r2 in
                               λn.((2 * n * r1) ÷ k)
               else if (p * 2 * (n + 1)) < ((-1) * 4 * (n + 1))
                       then eval r = near-root(i;p;4 * (n + 1);2 * (n + 1)) in
                            let r1,r2 = r 
                            in eval k = r2 in
                               λn.((2 * n * r1) ÷ k)
                       else (λk.(2 * k * 0))
        , λk.(k - 1)
        > }

---

Latex:

---

Latex:
No  Annotations
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .
    \mexists{}q:\{q:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}| 
            (\mforall{}n,m:\mBbbN{}.    (((r0  \mleq{}  (q  n))  \mwedge{}  (r0  \mleq{}  (q  m)))  \mvee{}  (((q  n)  \mleq{}  r0)  \mwedge{}  ((q  m)  \mleq{}  r0))))
            \mwedge{}  ((\muparrow{}isEven(i))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  (r0  \mleq{}  (q  m))))\} 
      lim  n\mrightarrow{}\minfty{}.q  n\^{}i  =  x


By

---

Latex:
Extract  of  Obid:  rroot-exists1
not  unfolding    divide  near-root  rlessw  mu-ge  absval
finishing  with  Auto
normalizes  to:

\mlambda{}i,x.  eval  xx  =  x  in
            <\mlambda{}n.eval  p  =  xx  (2  *  (n  +  1))  in
                    if  (1  *  4  *  (n  +  1))  <  (p  *  2  *  (n  +  1))
                          then  if  (p  *  2  *  (n  +  1))  <  ((-1)  *  4  *  (n  +  1))
                                          then  eval  r  =  near-root(i;p;4  *  (n  +  1);2  *  (n  +  1))  in
                                                    let  r1,r2  =  r 
                                                    in  eval  k  =  r2  in
                                                          \mlambda{}n.((2  *  n  *  r1)  \mdiv{}  k)
                                          else  eval  r  =  near-root(i;p;4  *  (n  +  1);2  *  (n  +  1))  in
                                                    let  r1,r2  =  r 
                                                    in  eval  k  =  r2  in
                                                          \mlambda{}n.((2  *  n  *  r1)  \mdiv{}  k)
                          else  if  (p  *  2  *  (n  +  1))  <  ((-1)  *  4  *  (n  +  1))
                                          then  eval  r  =  near-root(i;p;4  *  (n  +  1);2  *  (n  +  1))  in
                                                    let  r1,r2  =  r 
                                                    in  eval  k  =  r2  in
                                                          \mlambda{}n.((2  *  n  *  r1)  \mdiv{}  k)
                                          else  (\mlambda{}k.(2  *  k  *  0))
            ,  \mlambda{}k.(k  -  1)
            >

---

Home Index