---

Step * 1 1 of Lemma implies-regular


1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. n : ℕ+
4. m : ℕ+
5. |(r(x n))/2 * n - (r(x m))/2 * 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)
⊢ |(m * (x n)) - n * (x m)| ≤ ((2 * k) * (n + m))
BY
{ ((Assert ((r(x n))/2 * n - (r(x m))/2 * m) = (r((m * (x n)) - n * (x m))/r(2 * n * m)) BY
          ((RWO "int-rdiv-req" 0 THENA Auto) THEN nRMul ⌜r(2 * n * m)⌝ 0⋅ THEN Auto))
   THEN (RWO "-1" (-5) THENA Auto)
   ) }

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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  m  :  \mBbbN{}\msupplus{}
5.  |(r(x  n))/2  *  n  -  (r(x  m))/2  *  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)
\mvdash{}  |(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  k)  *  (n  +  m))


By

---

Latex:
((Assert  ((r(x  n))/2  *  n  -  (r(x  m))/2  *  m)  =  (r((m  *  (x  n))  -  n  *  (x  m))/r(2  *  n  *  m))  BY
                ((RWO  "int-rdiv-req"  0  THENA  Auto)  THEN  nRMul  \mkleeneopen{}r(2  *  n  *  m)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (RWO  "-1"  (-5)  THENA  Auto)
  )

---

Home Index