---

Step * 1 of Lemma rabs-diff-rmul


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))
BY
{ (nRMul ⌜|a|⌝ (-2)⋅ THEN nRMul ⌜|d|⌝ (-3)⋅) }

1
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))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  d  :  \mBbbR{}
5.  x  :  \mBbbR{}
6.  y  :  \mBbbR{}
7.  |a  -  b|  \mleq{}  x
8.  |c  -  d|  \mleq{}  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:
(nRMul  \mkleeneopen{}|a|\mkleeneclose{}  (-2)\mcdot{}  THEN  nRMul  \mkleeneopen{}|d|\mkleeneclose{}  (-3)\mcdot{})

---

Home Index