---

Step * 1 of Lemma blend-close-reals

.....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))))
BY
{ (Auto
   THEN (Assert |(m * (x n)) - n * (y m)| ≤ (|(m * (x n)) - n * (x m)| + |(n * (x m)) - n * (y m)|) BY
               (RWO "int-triangle-inequality<" 0 THEN Auto))
   THEN Unfold `regular-int-seq` 7
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "7" 0 THENA Auto)
   THEN (Assert ⌜|(n * (x m)) - n * (y m)| ≤ (4 * (n + m))⌝⋅ THENM (RWO "-1" 0 THEN Auto))
   THEN Thin (-1)) }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  [k]  :  \mBbbN{}\msupplus{}
\mvdash{}  \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))))


By

---

Latex:
(Auto
  THEN  (Assert  |(m  *  (x  n))  -  n  *  (y  m)|  \mleq{}  (|(m  *  (x  n))  -  n  *  (x  m)|  +  |(n  *  (x  m))  -  n  *  (y  m)|)  BY
                          (RWO  "int-triangle-inequality<"  0  THEN  Auto))
  THEN  Unfold  `regular-int-seq`  7
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "7"  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}|(n  *  (x  m))  -  n  *  (y  m)|  \mleq{}  (4  *  (n  +  m))\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))
  THEN  Thin  (-1))

---

Home Index