---

Step * of Lemma implies-close-reals

∀[x,y:ℝ]. ∀[m:ℕ+]. ∀[k:ℕ].  ((|(x m) - y m| ≤ (2 * k)) ⇒ (|x - y| ≤ (r(2 + k)/r(m))))
BY
{ ((Auto
    THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜m⌝]⋅ THENA Auto)
    THEN (InstLemma `rational-approx-property` [⌜y⌝;⌜m⌝]⋅ THENA Auto))
   THEN (Assert ⌜|(x within 1/m) - (y within 1/m)| ≤ (r(k)/r(m))⌝⋅
        THENM UseTriangleInequality [⌜(x within 1/m)⌝;⌜(y within 1/m)⌝]⋅
        )
   ) }

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

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

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[k:\mBbbN{}].    ((|(x  m)  -  y  m|  \mleq{}  (2  *  k))  {}\mRightarrow{}  (|x  -  y|  \mleq{}  (r(2  +  k)/r(m))))


By

---

Latex:
((Auto
    THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}|(x  within  1/m)  -  (y  within  1/m)|  \mleq{}  (r(k)/r(m))\mkleeneclose{}\mcdot{}
            THENM  UseTriangleInequality  [\mkleeneopen{}(x  within  1/m)\mkleeneclose{};\mkleeneopen{}(y  within  1/m)\mkleeneclose{}]\mcdot{}
            )
  )

---

Home Index