---

Step * 2 of Lemma rmul_functionality_wrt_rleq2


1. x : ℝ
2. y : ℝ
3. z : ℝ
4. w : ℝ
5. (r0 ≤ w) ∧ (r0 ≤ z)
6. x ≤ z
7. w ≤ y
⊢ (x * w) ≤ (z * y)
BY
{ (((InstLemma `rmul_functionality_wrt_rleq` [⌜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) ∧ (r0 ≤ z)
6. x ≤ z
7. w ≤ y
8. (x * w) ≤ (z * w)
9. (w * z) ≤ (y * z)
⊢ (x * w) ≤ (z * y)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  z  :  \mBbbR{}
4.  w  :  \mBbbR{}
5.  (r0  \mleq{}  w)  \mwedge{}  (r0  \mleq{}  z)
6.  x  \mleq{}  z
7.  w  \mleq{}  y
\mvdash{}  (x  *  w)  \mleq{}  (z  *  y)


By

---

Latex:
(((InstLemma  `rmul\_functionality\_wrt\_rleq`  [\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