---

Step * of Lemma reciprocal-qle

∀e:ℚ. ∃m:ℕ+. ((1/m) ≤ e) supposing 0 < e
BY
{ Extract of Obid: reciprocal-qle-proof
  not unfolding  qrep divide
  finishing with Auto
  normalizes to:
  
  λe.let v1,v2 = qrep(e) 
     in if v1=1 then <v2, Ax> else <(v2 ÷ v1) + 1, Ax> }

---

Latex:

---

Latex:
\mforall{}e:\mBbbQ{}.  \mexists{}m:\mBbbN{}\msupplus{}.  ((1/m)  \mleq{}  e)  supposing  0  <  e


By

---

Latex:
Extract  of  Obid:  reciprocal-qle-proof
not  unfolding    qrep  divide
finishing  with  Auto
normalizes  to:

\mlambda{}e.let  v1,v2  =  qrep(e) 
      in  if  v1=1  then  <v2,  Ax>  else  <(v2  \mdiv{}  v1)  +  1,  Ax>

---

Home Index