---

Step * 1 of Lemma close-reals-implies


1. x : ℝ
2. y : ℝ
3. m : ℕ+
4. (|(x m) - y m| * 3 * m) ≤ ((4 * 3 * m) + (2 * m))
⊢ |(x m) - y m| ≤ 4
BY
{ (SupposeNot THEN (Assert 5 ≤ |(x m) - y m| BY Auto) THEN Mul ⌜3 * m⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  m  :  \mBbbN{}\msupplus{}
4.  (|(x  m)  -  y  m|  *  3  *  m)  \mleq{}  ((4  *  3  *  m)  +  (2  *  m))
\mvdash{}  |(x  m)  -  y  m|  \mleq{}  4


By

---

Latex:
(SupposeNot  THEN  (Assert  5  \mleq{}  |(x  m)  -  y  m|  BY  Auto)  THEN  Mul  \mkleeneopen{}3  *  m\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index