---

Step * of Lemma approximate-qsqrt-ext

∀a:{a:ℚ| 0 ≤ a} . ∀n:ℕ+.  (∃q:ℚ [((0 ≤ q) ∧ |(q * q) - a| < (1/n))])
BY
{ Extract of Obid: approximate-qsqrt
  not unfolding  qmul isqrt qdiv qrep divide
  finishing with Auto
  normalizes to:
  
  λa,n. let v1,v2 = qrep(a) 
        in eval na = (v1 * n) ÷ v2 in
           if (na) < (n - 1)
              then (isqrt((4 * n) * na) + 1/2 * n)
              else eval c = isqrt(((na + 1) ÷ n) + 1) + 1 in
                   c * (isqrt((4 * (c * c) * n) * na) + 1/2 * (c * c) * n) }

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbQ{}|  0  \mleq{}  a\}  .  \mforall{}n:\mBbbN{}\msupplus{}.    (\mexists{}q:\mBbbQ{}  [((0  \mleq{}  q)  \mwedge{}  |(q  *  q)  -  a|  <  (1/n))])


By

---

Latex:
Extract  of  Obid:  approximate-qsqrt
not  unfolding    qmul  isqrt  qdiv  qrep  divide
finishing  with  Auto
normalizes  to:

\mlambda{}a,n.  let  v1,v2  =  qrep(a) 
            in  eval  na  =  (v1  *  n)  \mdiv{}  v2  in
                  if  (na)  <  (n  -  1)
                        then  (isqrt((4  *  n)  *  na)  +  1/2  *  n)
                        else  eval  c  =  isqrt(((na  +  1)  \mdiv{}  n)  +  1)  +  1  in
                                  c  *  (isqrt((4  *  (c  *  c)  *  n)  *  na)  +  1/2  *  (c  *  c)  *  n)

---

Home Index