---

Step * of Lemma rmul-nonneg-case1

∀[x,y:ℝ].  r0 ≤ (x * y) supposing (r0 ≤ x) ∧ (r0 ≤ y)
BY
{ (InstLemma `rmul-nonneg` [] THEN RepeatFor 3 (ParallelLast) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rmul-nonneg`  []  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index