---

Step * of Lemma combine-rless

∀a,b,c,d:ℝ.  ((a < b) ⇒ (c < d) ⇒ (((b * c) + (a * d)) < ((b * d) + (a * c))))
BY
{ (Auto THEN (Assert r0 < ((b - a) * (d - c)) BY ((BLemma `rmul-is-positive` THENM OrLeft) THEN Auto)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b,c,d:\mBbbR{}.    ((a  <  b)  {}\mRightarrow{}  (c  <  d)  {}\mRightarrow{}  (((b  *  c)  +  (a  *  d))  <  ((b  *  d)  +  (a  *  c))))


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  ((b  -  a)  *  (d  -  c))  BY
                          ((BLemma  `rmul-is-positive`  THENM  OrLeft)  THEN  Auto))
  THEN  Auto)

---

Home Index