---

Step * of Lemma small-reciprocal-rneq-zero

∀x:ℝ. (x ≠ r0 ⇒ (∃k:ℕ+. ((r1/r(k)) < |x|)))
BY
{ (Auto THEN BLemma `small-reciprocal-real-ext` THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. x : ℝ@i
2. x ≠ r0@i
⊢ r0 < |x|

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `small-reciprocal-real-ext`  THEN  MemTypeCD  THEN  Auto)

---

Home Index