---

Step * of Lemma rmul_functionality_wrt_rleq2

∀[x,y,z,w:ℝ].  ((x * w) ≤ (z * y)) supposing ((w ≤ y) and (x ≤ z) and (((r0 ≤ x) ∧ (r0 ≤ y)) ∨ ((r0 ≤ w) ∧ (r0 ≤ z))))
BY
{ (Auto THEN D -3) }

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  -3)

---

Home Index