---

Step * 2 1 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. m : ℕ+
8. regular-seq(x)
9. regular-seq(y)
10. n < k
11. m < k
⊢ |(m * (x n)) - n * (x m)| ≤ (6 * (n + m))
BY
{ (Unfold `regular-int-seq` -4 THEN RWO  "-4" 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.  m  :  \mBbbN{}\msupplus{}
8.  regular-seq(x)
9.  regular-seq(y)
10.  n  <  k
11.  m  <  k
\mvdash{}  |(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  (6  *  (n  +  m))


By

---

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

---

Home Index