---

Step * of Lemma rmul_reverses_rleq_iff

∀[x,y,z:ℝ].  uiff(x ≤ z;(z * y) ≤ (x * y)) supposing y < r0
BY
{ Auto }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. y < r0
5. x ≤ z
⊢ (z * y) ≤ (x * y)

2
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. y < r0
5. (z * y) ≤ (x * y)
⊢ x ≤ z

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    uiff(x  \mleq{}  z;(z  *  y)  \mleq{}  (x  *  y))  supposing  y  <  r0


By

---

Latex:
Auto

---

Home Index