---

Step * 1 3 of Lemma int-rmul_wf


1. k : ℤ
2. ¬0 < k
3. ¬k < 0
4. a : ℕ+ ⟶ ℤ
5. ∀n,m:ℕ+.  (|(m * (a n)) - n * (a m)| ≤ ((2 * 1) * (n + m)))
6. n : ℕ+
7. m : ℕ+
⊢ |(m * 0) - n * 0| ≤ (2 * (n + m))
BY
{ ((RW IntNormC 0 THENA Auto) THEN RepUR ``absval`` 0 THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  \mneg{}0  <  k
3.  \mneg{}k  <  0
4.  a  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (a  n))  -  n  *  (a  m)|  \mleq{}  ((2  *  1)  *  (n  +  m)))
6.  n  :  \mBbbN{}\msupplus{}
7.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  |(m  *  0)  -  n  *  0|  \mleq{}  (2  *  (n  +  m))


By

---

Latex:
((RW  IntNormC  0  THENA  Auto)  THEN  RepUR  ``absval``  0  THEN  Auto')

---

Home Index