---

Step * of Lemma implies-real

∀[x:ℕ+ ⟶ ℤ]. x ∈ ℝ supposing ∀n,m:ℕ+.  (|(x within 1/n) - (x within 1/m)| ≤ ((r1/r(n)) + (r1/r(m))))
BY
{ (Auto THEN MemTypeCD THEN Auto THEN FLemma `implies-regular` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}]
    x  \mmember{}  \mBbbR{}  supposing  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(x  within  1/n)  -  (x  within  1/m)|  \mleq{}  ((r1/r(n))  +  (r1/r(m))))


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  FLemma  `implies-regular`  [-1]  THEN  Auto)

---

Home Index