---

Step * of Lemma absval-diff-product-bound

∀u,v,x,y:ℕ.  ((|u - v| * |x - y|) ≤ |(imax(u;v) * imax(x;y)) - imin(u;v) * imin(x;y)|)
BY
{ Assert ⌜∀u:ℕ. ∀v:ℕu. ∀x:ℕ. ∀y:ℕx.  ((|u - v| * |x - y|) ≤ |(u * x) - v * y|)⌝⋅ }

1
.....assertion..... 
∀u:ℕ. ∀v:ℕu. ∀x:ℕ. ∀y:ℕx.  ((|u - v| * |x - y|) ≤ |(u * x) - v * y|)

2
1. ∀u:ℕ. ∀v:ℕu. ∀x:ℕ. ∀y:ℕx.  ((|u - v| * |x - y|) ≤ |(u * x) - v * y|)
⊢ ∀u,v,x,y:ℕ.  ((|u - v| * |x - y|) ≤ |(imax(u;v) * imax(x;y)) - imin(u;v) * imin(x;y)|)

---

Latex:

---

Latex:
\mforall{}u,v,x,y:\mBbbN{}.    ((|u  -  v|  *  |x  -  y|)  \mleq{}  |(imax(u;v)  *  imax(x;y))  -  imin(u;v)  *  imin(x;y)|)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}u:\mBbbN{}.  \mforall{}v:\mBbbN{}u.  \mforall{}x:\mBbbN{}.  \mforall{}y:\mBbbN{}x.    ((|u  -  v|  *  |x  -  y|)  \mleq{}  |(u  *  x)  -  v  *  y|)\mkleeneclose{}\mcdot{}

---

Home Index