---

Step * 2 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))))
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))
BY
{ (InstHyp [⌜x⌝;⌜y⌝;⌜m⌝;⌜n⌝] 2⋅ THEN Auto) }

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. ¬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))

---

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
\mvdash{}  |(m  *  (y  n))  -  n  *  (x  m)|  \mleq{}  (6  *  (n  +  m))


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  2\mcdot{}  THEN  Auto)

---

Home Index