---

Step * of Lemma rmul_preserves_rleq

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index