---

Step * of Lemma q-archimedean-ext

∀a:ℚ. ∃n:ℕ. ((-(n) ≤ a) ∧ (a ≤ n))
BY
{ Extract of Obid: q-archimedean
  not unfolding  qrep divide
  finishing with Auto
  normalizes to:
  
  λa.let x,v2 = qrep(a) 
     in if (x) < (0)  then <(-(x ÷ v2)) + 1, Ax, Ax>  else <(x ÷ v2) + 1, Ax, Ax> }

---

Latex:

---

Latex:
\mforall{}a:\mBbbQ{}.  \mexists{}n:\mBbbN{}.  ((-(n)  \mleq{}  a)  \mwedge{}  (a  \mleq{}  n))


By

---

Latex:
Extract  of  Obid:  q-archimedean
not  unfolding    qrep  divide
finishing  with  Auto
normalizes  to:

\mlambda{}a.let  x,v2  =  qrep(a) 
      in  if  (x)  <  (0)    then  <(-(x  \mdiv{}  v2))  +  1,  Ax,  Ax>    else  <(x  \mdiv{}  v2)  +  1,  Ax,  Ax>

---

Home Index