---

Step * of Lemma close-reals-iff

No Annotations
∀[x,y:ℝ]. ∀[k:ℕ+].  uiff(|x - y| ≤ (r1/r(k));∀m:ℕ+. ((|(x m) - y m| * k) ≤ ((4 * k) + (2 * m))))
BY
{ Auto }

1
1. x : ℝ
2. y : ℝ
3. k : ℕ+
4. |x - y| ≤ (r1/r(k))
5. m : ℕ+
⊢ (|(x m) - y m| * k) ≤ ((4 * k) + (2 * m))

2
1. x : ℝ
2. y : ℝ
3. k : ℕ+
4. ∀m:ℕ+. ((|(x m) - y m| * k) ≤ ((4 * k) + (2 * m)))
⊢ |x - y| ≤ (r1/r(k))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].    uiff(|x  -  y|  \mleq{}  (r1/r(k));\mforall{}m:\mBbbN{}\msupplus{}.  ((|(x  m)  -  y  m|  *  k)  \mleq{}  ((4  *  k)  +  (2  *  m))))


By

---

Latex:
Auto

---

Home Index