---

Step * 2 3 of Lemma blend-close-reals


1. k : ℕ+
2. ∀x,y:ℝ. ∀n,m:ℕ+.
     ((|x - y| ≤ (r1/r(k))) ⇒ regular-seq(x) ⇒ n < k ⇒ (k ≤ m) ⇒ (|(m * (x n)) - n * (y m)| ≤ (6 * (n + m))))
3. x : ℝ
4. y : ℝ
5. |x - y| ≤ (r1/r(k))
6. n : ℕ+
7. ¬n < k
8. m : ℕ+
9. ¬m < k
10. regular-seq(x)
11. regular-seq(y)
⊢ |(m * (y n)) - n * (y m)| ≤ (6 * (n + m))
BY
{ (Unfold `regular-int-seq` -1 THEN RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  \mforall{}x,y:\mBbbR{}.  \mforall{}n,m:\mBbbN{}\msupplus{}.
          ((|x  -  y|  \mleq{}  (r1/r(k)))
          {}\mRightarrow{}  regular-seq(x)
          {}\mRightarrow{}  n  <  k
          {}\mRightarrow{}  (k  \mleq{}  m)
          {}\mRightarrow{}  (|(m  *  (x  n))  -  n  *  (y  m)|  \mleq{}  (6  *  (n  +  m))))
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  |x  -  y|  \mleq{}  (r1/r(k))
6.  n  :  \mBbbN{}\msupplus{}
7.  \mneg{}n  <  k
8.  m  :  \mBbbN{}\msupplus{}
9.  \mneg{}m  <  k
10.  regular-seq(x)
11.  regular-seq(y)
\mvdash{}  |(m  *  (y  n))  -  n  *  (y  m)|  \mleq{}  (6  *  (n  +  m))


By

---

Latex:
(Unfold  `regular-int-seq`  -1  THEN  RWO    "-1"  0  THEN  Auto)

---

Home Index