---

Step * 2 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. ¬n < k
8. m : ℕ+
9. regular-seq(x)
10. regular-seq(y)
11. m < k
12. |(n * (x m)) - m * (y n)| ≤ (6 * (m + n))
⊢ |(m * (y n)) - n * (x m)| ≤ (6 * (n + m))
BY
{ ((Subst' (m * (y n)) - n * (x m) ~ -((n * (x m)) - m * (y n)) 0 THENA Auto) THEN RWO "absval-minus" 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.  regular-seq(x)
10.  regular-seq(y)
11.  m  <  k
12.  |(n  *  (x  m))  -  m  *  (y  n)|  \mleq{}  (6  *  (m  +  n))
\mvdash{}  |(m  *  (y  n))  -  n  *  (x  m)|  \mleq{}  (6  *  (n  +  m))


By

---

Latex:
((Subst'  (m  *  (y  n))  -  n  *  (x  m)  \msim{}  -((n  *  (x  m))  -  m  *  (y  n))  0  THENA  Auto)
  THEN  RWO  "absval-minus"  0
  THEN  Auto)

---

Home Index