---

Step * 1 of Lemma rmul-int


1. a : ℤ
2. b : ℤ
3. n : ℕ+@i
⊢ |(((2 * n * a) * 2 * n * b) ÷ 2 * n) - 2 * n * a * b| ≤ 0
BY
{ (Subst ⌜(2 * n * a) * 2 * n * b ~ (2 * n * a * b) * 2 * n⌝ 0⋅ THEN Auto THEN RWO "div-cancel" 0 THEN Auto) }

1
1. a : ℤ
2. b : ℤ
3. n : ℕ+@i
⊢ |(2 * n * a * b) - 2 * n * a * b| ≤ 0

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  |(((2  *  n  *  a)  *  2  *  n  *  b)  \mdiv{}  2  *  n)  -  2  *  n  *  a  *  b|  \mleq{}  0


By

---

Latex:
(Subst  \mkleeneopen{}(2  *  n  *  a)  *  2  *  n  *  b  \msim{}  (2  *  n  *  a  *  b)  *  2  *  n\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  RWO  "div-cancel"  0
  THEN  Auto)

---

Home Index