---

Step * 1 of Lemma absval-diff-product-bound

.....assertion..... 
∀u:ℕ. ∀v:ℕu. ∀x:ℕ. ∀y:ℕx.  ((|u - v| * |x - y|) ≤ |(u * x) - v * y|)
BY
{ (UnivCD THENA Auto) }

1
1. u : ℕ
2. v : ℕu
3. x : ℕ
4. y : ℕx
⊢ (|u - v| * |x - y|) ≤ |(u * x) - v * y|

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}u:\mBbbN{}.  \mforall{}v:\mBbbN{}u.  \mforall{}x:\mBbbN{}.  \mforall{}y:\mBbbN{}x.    ((|u  -  v|  *  |x  -  y|)  \mleq{}  |(u  *  x)  -  v  *  y|)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index