---

Step * 1 of Lemma rmul_functionality_wrt_rleq2


1. x : ℝ
2. y : ℝ
3. z : ℝ
4. w : ℝ
5. (r0 ≤ x) ∧ (r0 ≤ y)
6. x ≤ z
7. w ≤ y
⊢ (x * w) ≤ (z * y)
BY
{ (((InstLemma `rmul_functionality_wrt_rleq` [⌜w⌝; ⌜x⌝; ⌜y⌝])⋅ THENA Auto)
   THEN ((InstLemma `rmul_functionality_wrt_rleq` [⌜x⌝; ⌜y⌝; ⌜z⌝])⋅ THENA Auto)
   THEN skip{(All nRNorm THEN Auto)}) }

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index