---

Step * 2 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))))
⊢ ∀[x,y:ℝ].  ((|x - y| ≤ (r1/r(k))) ⇒ 3-regular-seq(blend-seq(k;x;y)))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert regular-seq(x) BY
               (DVar `x' THEN Unhide THEN Auto))
   THEN (Assert regular-seq(y) BY
               (DVar `y' THEN Unhide THEN Auto))
   THEN RepUR ``blend-seq`` 0
   THEN RepeatFor 2 (AutoSplit)) }

1
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))

2
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. regular-seq(x)
10. regular-seq(y)
11. m < k
⊢ |(m * (y n)) - n * (x m)| ≤ (6 * (n + m))

3
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))

---

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))))
\mvdash{}  \mforall{}[x,y:\mBbbR{}].    ((|x  -  y|  \mleq{}  (r1/r(k)))  {}\mRightarrow{}  3-regular-seq(blend-seq(k;x;y)))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  regular-seq(x)  BY
                          (DVar  `x'  THEN  Unhide  THEN  Auto))
  THEN  (Assert  regular-seq(y)  BY
                          (DVar  `y'  THEN  Unhide  THEN  Auto))
  THEN  RepUR  ``blend-seq``  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index