---

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


1. ∀u:ℕ. ∀v:ℕu. ∀x:ℕ. ∀y:ℕx.  ((|u - v| * |x - y|) ≤ |(u * x) - v * y|)
2. u : ℕ
3. v : ℕ
4. x : ℕ
5. y : ℕ
6. ¬(u = v ∈ ℤ)
7. ¬(x = y ∈ ℤ)
⊢ (|u - v| * |x - y|) ≤ |(imax(u;v) * imax(x;y)) - imin(u;v) * imin(x;y)|
BY
{ ((RWO "imax_unfold imin_unfold" 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN RWO "1<" 0
   THEN Auto
   THEN (BLemma `le_weakening` THEN Auto)
   THEN EqCD
   THEN Auto
   THEN RW  (AddrC [2] (LemmaC `absval-diff-symmetry`)) 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}u:\mBbbN{}.  \mforall{}v:\mBbbN{}u.  \mforall{}x:\mBbbN{}.  \mforall{}y:\mBbbN{}x.    ((|u  -  v|  *  |x  -  y|)  \mleq{}  |(u  *  x)  -  v  *  y|)
2.  u  :  \mBbbN{}
3.  v  :  \mBbbN{}
4.  x  :  \mBbbN{}
5.  y  :  \mBbbN{}
6.  \mneg{}(u  =  v)
7.  \mneg{}(x  =  y)
\mvdash{}  (|u  -  v|  *  |x  -  y|)  \mleq{}  |(imax(u;v)  *  imax(x;y))  -  imin(u;v)  *  imin(x;y)|


By

---

Latex:
((RWO  "imax\_unfold  imin\_unfold"  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  RWO  "1<"  0
  THEN  Auto
  THEN  (BLemma  `le\_weakening`  THEN  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  RW    (AddrC  [2]  (LemmaC  `absval-diff-symmetry`))  0
  THEN  Auto)

---

Home Index