---

Step * of Lemma rmul_preserves_rleq3

∀[x,y,a,b:ℝ].  ((x * y) ≤ (a * b)) supposing ((x ≤ a) and (y ≤ b) and ((r0 ≤ x) ∧ (r0 ≤ y)))
BY
{ (Auto THEN nRMul ⌜a⌝ (-2)⋅ THEN (RWO "-2<" 0 THENA Auto) THEN nRMul ⌜y⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  nRMul  \mkleeneopen{}a\mkleeneclose{}  (-2)\mcdot{}  THEN  (RWO  "-2<"  0  THENA  Auto)  THEN  nRMul  \mkleeneopen{}y\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index