---

Step * of Lemma rmul_functionality_wrt_rleq

∀[x,y,z:ℝ].  ((x * y) ≤ (z * y)) supposing ((r0 ≤ y) and (x ≤ z))
BY
{ (RepUR ``rleq`` 0 THEN Auto THEN ((FLemma `rnonneg-rmul` [-2; -1]) THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    ((x  *  y)  \mleq{}  (z  *  y))  supposing  ((r0  \mleq{}  y)  and  (x  \mleq{}  z))


By

---

Latex:
(RepUR  ``rleq``  0  THEN  Auto  THEN  ((FLemma  `rnonneg-rmul`  [-2;  -1])  THENA  Auto))

---

Home Index