---

Step * of Lemma near-root-rational-ext

∀k:{2...}. ∀p:{p:ℤ| (0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.
  (∃r:ℤ × ℕ+ [let a,b = r 
              in (0 ≤ p ⇐⇒ 0 ≤ a) ∧ (|(r(a))/b^k - (r(p)/r(q))| < (r1/r(n)))])
BY
{ Extract of Obid: near-root-rational
  not unfolding  divide absval iroot fastexp
  finishing with (Try (Fold `near-root` 0) THEN Auto)
  normalizes to:
  
  λk,p,q,n. near-root(k;p;q;n) }

---

Latex:

---

Latex:
\mforall{}k:\{2...\}.  \mforall{}p:\{p:\mBbbZ{}|  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}q,n:\mBbbN{}\msupplus{}.
    (\mexists{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  [let  a,b  =  r 
                            in  (0  \mleq{}  p  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  a)  \mwedge{}  (|(r(a))/b\^{}k  -  (r(p)/r(q))|  <  (r1/r(n)))])


By

---

Latex:
Extract  of  Obid:  near-root-rational
not  unfolding    divide  absval  iroot  fastexp
finishing  with  (Try  (Fold  `near-root`  0)  THEN  Auto)
normalizes  to:

\mlambda{}k,p,q,n.  near-root(k;p;q;n)

---

Home Index