---

Step * of Lemma qroot-ext

∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+.  (∃q:ℚ [((0 ≤ a ⇐⇒ 0 ≤ q) ∧ |q ↑ k - a| < (1/n))])
BY
{ Extract of Obid: qroot
  not unfolding  qmul iroot qdiv qrep fastexp
  finishing with Auto
  normalizes to:
  
  λk,a,n. let x,y = qrep(a) 
          in if y=1
             then if n=1
                  then eval c = 2^k - 1 in
                       eval a = x * 2 * c in
                       eval d = (2 * c) - 1 in
                       eval x1 = iroot(k;eval x = a in if (0) < (x)  then x + d  else ((-x) + d)) + 1 in
                         let x1,r = divrem(k * 2 * x1^k - 1; d) 
                         in eval x1 = x1 + 1 in
                            let x2,r = divrem(iroot(k;eval x = a in
                                                      if (0) < (x)  then (x + d) * x1^k  else (((-x) + d) * x1^k));
                                              2) 
                            in eval x2 = x2 in
                               (if (x) < (0)  then -x2  else x2/x1)
                  else eval b = y * n in
                       eval c = b^k - 1 in
                       eval a = x * n * c in
                       eval d = c - 1 in
                       eval x1 = iroot(k;eval x = a in if (0) < (x)  then x + d  else ((-x) + d)) + 1 in
                         let x1,r = divrem(k * b * x1^k - 1; d) 
                         in eval x1 = x1 + 1 in
                            let x2,r = divrem(iroot(k;eval x = a in
                                                      if (0) < (x)  then (x + d) * x1^k  else (((-x) + d) * x1^k));
                                              b) 
                            in eval x2 = x2 in
                               (if (x) < (0)  then -x2  else x2/x1)
             else eval b = y * n in
                  eval c = b^k - 1 in
                  eval a = x * n * c in
                  eval d = c - 1 in
                  eval x1 = iroot(k;eval x = a in if (0) < (x)  then x + d  else ((-x) + d)) + 1 in
                    let x1,r = divrem(k * b * x1^k - 1; d) 
                    in eval x1 = x1 + 1 in
                       let x2,r = divrem(iroot(k;eval x = a in
                                                 if (0) < (x)  then (x + d) * x1^k  else (((-x) + d) * x1^k));
                                         b) 
                       in eval x2 = x2 in
                          (if (x) < (0)  then -x2  else x2/x1) }

---

Latex:

---

Latex:
\mforall{}k:\{2...\}.  \mforall{}a:\{a:\mBbbQ{}|  (0  \mleq{}  a)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
    (\mexists{}q:\mBbbQ{}  [((0  \mleq{}  a  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  q)  \mwedge{}  |q  \muparrow{}  k  -  a|  <  (1/n))])


By

---

Latex:
Extract  of  Obid:  qroot
not  unfolding    qmul  iroot  qdiv  qrep  fastexp
finishing  with  Auto
normalizes  to:

\mlambda{}k,a,n.  let  x,y  =  qrep(a) 
                in  if  y=1
                      then  if  n=1
                                then  eval  c  =  2\^{}k  -  1  in
                                          eval  a  =  x  *  2  *  c  in
                                          eval  d  =  (2  *  c)  -  1  in
                                          eval  x1  =  iroot(k;eval  x  =  a  in  if  (0)  <  (x)    then  x  +  d    else  ((-x)  +  d))  +  1  \000Cin
                                              let  x1,r  =  divrem(k  *  2  *  x1\^{}k  -  1;  d) 
                                              in  eval  x1  =  x1  +  1  in
                                                    let  x2,r  =  divrem(iroot(k;eval  x  =  a  in
                                                                                                        if  (0)  <  (x)
                                                                                                              then  (x  +  d)  *  x1\^{}k
                                                                                                              else  (((-x)  +  d)  *  x1\^{}k));
                                                                                        2) 
                                                    in  eval  x2  =  x2  in
                                                          (if  (x)  <  (0)    then  -x2    else  x2/x1)
                                else  eval  b  =  y  *  n  in
                                          eval  c  =  b\^{}k  -  1  in
                                          eval  a  =  x  *  n  *  c  in
                                          eval  d  =  c  -  1  in
                                          eval  x1  =  iroot(k;eval  x  =  a  in  if  (0)  <  (x)    then  x  +  d    else  ((-x)  +  d))  +  1  \000Cin
                                              let  x1,r  =  divrem(k  *  b  *  x1\^{}k  -  1;  d) 
                                              in  eval  x1  =  x1  +  1  in
                                                    let  x2,r  =  divrem(iroot(k;eval  x  =  a  in
                                                                                                        if  (0)  <  (x)
                                                                                                              then  (x  +  d)  *  x1\^{}k
                                                                                                              else  (((-x)  +  d)  *  x1\^{}k));
                                                                                        b) 
                                                    in  eval  x2  =  x2  in
                                                          (if  (x)  <  (0)    then  -x2    else  x2/x1)
                      else  eval  b  =  y  *  n  in
                                eval  c  =  b\^{}k  -  1  in
                                eval  a  =  x  *  n  *  c  in
                                eval  d  =  c  -  1  in
                                eval  x1  =  iroot(k;eval  x  =  a  in  if  (0)  <  (x)    then  x  +  d    else  ((-x)  +  d))  +  1  in
                                    let  x1,r  =  divrem(k  *  b  *  x1\^{}k  -  1;  d) 
                                    in  eval  x1  =  x1  +  1  in
                                          let  x2,r  =  divrem(iroot(k;eval  x  =  a  in
                                                                                              if  (0)  <  (x)
                                                                                                    then  (x  +  d)  *  x1\^{}k
                                                                                                    else  (((-x)  +  d)  *  x1\^{}k));
                                                                              b) 
                                          in  eval  x2  =  x2  in
                                                (if  (x)  <  (0)    then  -x2    else  x2/x1)

---

Home Index