---

Step * 1 1 1 1 1 1 of Lemma real-approx


1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
4. k : ℕ+
5. 1 ≤ n
6. (k * 1) ≤ (k * n)
7. m : {2 * n * k...}
⊢ ((-2) * m) ≤ (((-1) * k * |((-1) * m * (x n)) + (n * (x m))| * |2|) + (4 * k * m))
BY
{ TACTIC:(Assert |(n * (x m)) - m * (x n)| ≤ ((2 * 1) * (m + n)) BY
                (D 1 THEN Unhide THEN Auto)) }

1
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
4. k : ℕ+
5. 1 ≤ n
6. (k * 1) ≤ (k * n)
7. m : {2 * n * k...}
8. |(n * (x m)) - m * (x n)| ≤ ((2 * 1) * (m + n))
⊢ ((-2) * m) ≤ (((-1) * k * |((-1) * m * (x n)) + (n * (x m))| * |2|) + (4 * k * m))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  r(2  *  n)  =  |r(2  *  n)|
4.  k  :  \mBbbN{}\msupplus{}
5.  1  \mleq{}  n
6.  (k  *  1)  \mleq{}  (k  *  n)
7.  m  :  \{2  *  n  *  k...\}
\mvdash{}  ((-2)  *  m)  \mleq{}  (((-1)  *  k  *  |((-1)  *  m  *  (x  n))  +  (n  *  (x  m))|  *  |2|)  +  (4  *  k  *  m))


By

---

Latex:
TACTIC:(Assert  |(n  *  (x  m))  -  m  *  (x  n)|  \mleq{}  ((2  *  1)  *  (m  +  n))  BY
                            (D  1  THEN  Unhide  THEN  Auto))

---

Home Index