---

Step * of Lemma rabs-diff-rmul

∀[a,b,c,d,x,y:ℝ].  ((|a - b| ≤ x) ⇒ (|c - d| ≤ y) ⇒ (|(a * c) - b * d| ≤ ((|a| * y) + (|d| * x))))
BY
{ (Auto
   THEN (Assert ((a * c) - b * d) = ((a * (c - d)) + (d * (a - b))) BY
               Auto)
   THEN (RWW "-1 r-triangle-inequality rabs-rmul" 0 THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. d : ℝ
5. x : ℝ
6. y : ℝ
7. |a - b| ≤ x
8. |c - d| ≤ y
9. ((a * c) - b * d) = ((a * (c - d)) + (d * (a - b)))
⊢ ((|a| * |c - d|) + (|d| * |a - b|)) ≤ ((|a| * y) + (|d| * x))

---

Latex:

---

Latex:
\mforall{}[a,b,c,d,x,y:\mBbbR{}].    ((|a  -  b|  \mleq{}  x)  {}\mRightarrow{}  (|c  -  d|  \mleq{}  y)  {}\mRightarrow{}  (|(a  *  c)  -  b  *  d|  \mleq{}  ((|a|  *  y)  +  (|d|  *  x))))


By

---

Latex:
(Auto
  THEN  (Assert  ((a  *  c)  -  b  *  d)  =  ((a  *  (c  -  d))  +  (d  *  (a  -  b)))  BY
                          Auto)
  THEN  (RWW  "-1  r-triangle-inequality  rabs-rmul"  0  THENA  Auto))

---

Home Index