---

Step * of Lemma integer-nth-root-ext

∀n:ℕ+. ∀x:ℕ.  (∃r:ℕ [((r^n ≤ x) ∧ x < (r + 1)^n)])
BY
{ Extract of Obid: integer-nth-root
  not unfolding  primrec exp fastexp divide
  finishing with Auto
  normalizes to:
  
  λn.eval b = 2^n in
     λi.letrec rec(i)=if i=0
                      then 0
                      else eval j = i ÷ b in
                           eval r2 = 2 * (rec j) in
                           eval r2' = r2 + 1 in
                             if (r2'^n) < (i + 1)  then r2'  else r2 in
         rec(i) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbN{}.    (\mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)\^{}n)])


By

---

Latex:
Extract  of  Obid:  integer-nth-root
not  unfolding    primrec  exp  fastexp  divide
finishing  with  Auto
normalizes  to:

\mlambda{}n.eval  b  =  2\^{}n  in
      \mlambda{}i.letrec  rec(i)=if  i=0
                                        then  0
                                        else  eval  j  =  i  \mdiv{}  b  in
                                                  eval  r2  =  2  *  (rec  j)  in
                                                  eval  r2'  =  r2  +  1  in
                                                      if  (r2'\^{}n)  <  (i  +  1)    then  r2'    else  r2  in
              rec(i)

---

Home Index