---

Step * of Lemma small-reciprocal-real-ext

∀x:{x:ℝ| r0 < x} . ∃k:ℕ+. ((r1/r(k)) < x)
BY
{ Extract of Obid: small-reciprocal-real
  not unfolding  rlessw rdiv int-to-real
  finishing with Auto
  normalizes to:
  
  λx.eval n = rlessw(r0;x) in
     <n + 1, rlessw((r1/r(n + 1));x)> }

---

Latex:

---

Latex:
\mforall{}x:\{x:\mBbbR{}|  r0  <  x\}  .  \mexists{}k:\mBbbN{}\msupplus{}.  ((r1/r(k))  <  x)


By

---

Latex:
Extract  of  Obid:  small-reciprocal-real
not  unfolding    rlessw  rdiv  int-to-real
finishing  with  Auto
normalizes  to:

\mlambda{}x.eval  n  =  rlessw(r0;x)  in
      <n  +  1,  rlessw((r1/r(n  +  1));x)>

---

Home Index