---

Step * of Lemma rmul_functionality_wrt_rless

∀x,y,z:ℝ.  ((x < z) ⇒ (r0 < y) ⇒ ((x * y) < (z * y)))
BY
{ (Auto
   THEN (UseWitness ⌜rlessw(x * y;z * y)⌝⋅ THEN Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (All (RWO "rless-iff-rpositive") THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. rpositive(z - x)
5. rpositive(y - r0)
⊢ rpositive((z * y) - x * y)

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbR{}.    ((x  <  z)  {}\mRightarrow{}  (r0  <  y)  {}\mRightarrow{}  ((x  *  y)  <  (z  *  y)))


By

---

Latex:
(Auto
  THEN  (UseWitness  \mkleeneopen{}rlessw(x  *  y;z  *  y)\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (All  (RWO  "rless-iff-rpositive")  THENA  Auto))

---

Home Index