---

Step * of Lemma blend-close-reals

∀[k:ℕ+]. ∀[x,y:ℝ].  ((|x - y| ≤ (r1/r(k))) ⇒ 3-regular-seq(blend-seq(k;x;y)))
BY
{ (Intro
   THEN Assert ⌜∀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))))⌝⋅
   ) }

1
.....assertion..... 
1. [k] : ℕ+
⊢ ∀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))))

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))))
⊢ ∀[x,y:ℝ].  ((|x - y| ≤ (r1/r(k))) ⇒ 3-regular-seq(blend-seq(k;x;y)))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x,y:\mBbbR{}].    ((|x  -  y|  \mleq{}  (r1/r(k)))  {}\mRightarrow{}  3-regular-seq(blend-seq(k;x;y)))


By

---

Latex:
(Intro
  THEN  Assert  \mkleeneopen{}\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))))\mkleeneclose{}\mcdot{}
  )

---

Home Index