---

Step * 1 1 1 1 of Lemma implies-regular


1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. n : ℕ+
4. m : ℕ+
5. r(|(m * (x n)) - n * (x m)|) ≤ r((2 * k * m) + (2 * k * n))
6. r0 < r(n * m)
7. r0 < r(2 * n * m)
8. |r(2 * n * m)| = r(2 * n * m)
9. ((r(x n))/2 * n - (r(x m))/2 * m) = (r((m * (x n)) - n * (x m))/r(2 * n * m))
⊢ |(m * (x n)) - n * (x m)| ≤ ((2 * k) * (n + m))
BY
{ (RWO "rleq-int" (-5) THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  m  :  \mBbbN{}\msupplus{}
5.  r(|(m  *  (x  n))  -  n  *  (x  m)|)  \mleq{}  r((2  *  k  *  m)  +  (2  *  k  *  n))
6.  r0  <  r(n  *  m)
7.  r0  <  r(2  *  n  *  m)
8.  |r(2  *  n  *  m)|  =  r(2  *  n  *  m)
9.  ((r(x  n))/2  *  n  -  (r(x  m))/2  *  m)  =  (r((m  *  (x  n))  -  n  *  (x  m))/r(2  *  n  *  m))
\mvdash{}  |(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  k)  *  (n  +  m))


By

---

Latex:
(RWO  "rleq-int"  (-5)  THEN  Auto)

---

Home Index