---

Step * of Lemma close-reals-implies

∀[x,y:ℝ]. ∀[m:ℕ+].  |(x m) - y m| ≤ 4 supposing |x - y| ≤ (r1/r(3 * m))
BY
{ (Auto THEN (RWO "close-reals-iff" (-1) THENA Auto) THEN (D -1 With ⌜m⌝  THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. m : ℕ+
4. (|(x m) - y m| * 3 * m) ≤ ((4 * 3 * m) + (2 * m))
⊢ |(x m) - y m| ≤ 4

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[m:\mBbbN{}\msupplus{}].    |(x  m)  -  y  m|  \mleq{}  4  supposing  |x  -  y|  \mleq{}  (r1/r(3  *  m))


By

---

Latex:
(Auto  THEN  (RWO  "close-reals-iff"  (-1)  THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}m\mkleeneclose{}    THENA  Auto))

---

Home Index