---

Step * of Lemma small-reciprocal

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

---

Latex:

---

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


By

---

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

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

---

Home Index