---

Step * of Lemma rroot-exists-ext

No Annotations
∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} .  (∃y:ℝ [(((↑isEven(i)) ⇒ (r0 ≤ y)) ∧ (y^i = x))])
BY
{ Extract of Obid: rroot-exists
  not unfolding  divide near-root fastexp
  finishing with Auto
  normalizes to:
  
  λi,x. eval xx = x in
        λn.eval m = 4 * n in
           eval p = xx (2 * (((2 * m^i) - 1) + 1)) in
             if (1 * 4 * (((2 * m^i) - 1) + 1)) < (p * 2 * (((2 * m^i) - 1) + 1))
                then if (p * 2 * (((2 * m^i) - 1) + 1)) < ((-1) * 4 * (((2 * m^i) - 1) + 1))
                        then eval r = near-root(i;p;4 * (((2 * m^i) - 1) + 1);2 * (((2 * m^i) - 1) + 1)) in
                             let r1,r2 = r 
                             in eval k = r2 in
                                (2 * m * r1) ÷ k ÷ 4
                        else eval r = near-root(i;p;4 * (((2 * m^i) - 1) + 1);2 * (((2 * m^i) - 1) + 1)) in
                             let r1,r2 = r 
                             in eval k = r2 in
                                (2 * m * r1) ÷ k ÷ 4
                else if (p * 2 * (((2 * m^i) - 1) + 1)) < ((-1) * 4 * (((2 * m^i) - 1) + 1))
                        then eval r = near-root(i;p;4 * (((2 * m^i) - 1) + 1);2 * (((2 * m^i) - 1) + 1)) in
                             let r1,r2 = r 
                             in eval k = r2 in
                                (2 * m * r1) ÷ k ÷ 4
                        else ((2 * m * 0) ÷ 4) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .    (\mexists{}y:\mBbbR{}  [(((\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  y))  \mwedge{}  (y\^{}i  =  x))])


By

---

Latex:
Extract  of  Obid:  rroot-exists
not  unfolding    divide  near-root  fastexp
finishing  with  Auto
normalizes  to:

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

---

Home Index