---

Step * of Lemma rdiv_functionality_wrt_rleq2

∀[x,y,z,w:ℝ].  ((x/w) ≤ (z/y)) supposing ((x ≤ z) and (y ≤ w) and ((r0 < y) ∧ ((r0 ≤ x) ∨ (r0 ≤ z))))
BY
{ (Auto THEN (nRMul ⌜y⌝ 0⋅ THENA Auto) THEN (nRMul ⌜w⌝ 0⋅ THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (nRMul  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  (nRMul  \mkleeneopen{}w\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index