---

Step * of Lemma rmul_functionality_wrt_rless2

∀x,y,z,w:ℝ.  ((r0 < w) ⇒ (x < z) ⇒ (x * w) < (z * y) supposing w ≤ y supposing r0 ≤ z)
BY
{ (Auto
   THEN ((InstLemma `rmul_functionality_wrt_rless` [⌜x⌝; ⌜w⌝; ⌜z⌝])⋅ THENA Auto)
   THEN ((InstLemma `rmul_functionality_wrt_rleq` [⌜w⌝; ⌜z⌝; ⌜y⌝])⋅ THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. w : ℝ
5. r0 < w
6. r0 ≤ z
7. x < z
8. w ≤ y
9. (x * w) < (z * w)
10. (w * z) ≤ (y * z)
⊢ (x * w) < (z * y)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rmul\_functionality\_wrt\_rless`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}w\mkleeneclose{};  \mkleeneopen{}z\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `rmul\_functionality\_wrt\_rleq`  [\mkleeneopen{}w\mkleeneclose{};  \mkleeneopen{}z\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index