---

Step * 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 * n * m))| ≤ (r((k * m) + (k * n))/r(n * m))
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 "rabs-rdiv" (-5) THENA Auto) THEN (RWO "-2" (-5) THENA Auto) THEN (nRMul ⌜r(2 * n * m)⌝ (-5)⋅ THENA Auto)) }

1
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))

---

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))/r(2  *  n  *  m))|  \mleq{}  (r((k  *  m)  +  (k  *  n))/r(n  *  m))
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  "rabs-rdiv"  (-5)  THENA  Auto)
  THEN  (RWO  "-2"  (-5)  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(2  *  n  *  m)\mkleeneclose{}  (-5)\mcdot{}  THENA  Auto))

---

Home Index