---

Step * of Lemma absval-diff-product-bound2

∀u,v,x,y:ℤ.  (|(u * v) - x * y| ≤ ((|u| * |v - y|) + (|y| * |u - x|)))
BY
{ (Intros
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN (RWO "int-triangle-inequality<" 0 THENA Auto)
   THEN RW IntNormC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}u,v,x,y:\mBbbZ{}.    (|(u  *  v)  -  x  *  y|  \mleq{}  ((|u|  *  |v  -  y|)  +  (|y|  *  |u  -  x|)))


By

---

Latex:
(Intros
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  (RWO  "int-triangle-inequality<"  0  THENA  Auto)
  THEN  RW  IntNormC  0
  THEN  Auto)

---

Home Index