---

Step * 1 1 of Lemma rabs-diff-rmul


1. a : ℝ
2. b : ℝ
3. c : ℝ
4. d : ℝ
5. x : ℝ
6. y : ℝ
7. (|a + -(b)| * |d|) ≤ (|d| * x)
8. (|c + -(d)| * |a|) ≤ (|a| * y)
9. ((a * c) - b * d) = ((a * (c - d)) + (d * (a - b)))
⊢ ((|a| * |c - d|) + (|d| * |a - b|)) ≤ ((|a| * y) + (|d| * x))
BY
{ (nRNorm 0 THEN RWO  "7 8" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  d  :  \mBbbR{}
5.  x  :  \mBbbR{}
6.  y  :  \mBbbR{}
7.  (|a  +  -(b)|  *  |d|)  \mleq{}  (|d|  *  x)
8.  (|c  +  -(d)|  *  |a|)  \mleq{}  (|a|  *  y)
9.  ((a  *  c)  -  b  *  d)  =  ((a  *  (c  -  d))  +  (d  *  (a  -  b)))
\mvdash{}  ((|a|  *  |c  -  d|)  +  (|d|  *  |a  -  b|))  \mleq{}  ((|a|  *  y)  +  (|d|  *  x))


By

---

Latex:
(nRNorm  0  THEN  RWO    "7  8"  0  THEN  Auto)

---

Home Index