---

Step * of Lemma rmul_reverses_rless_iff

∀x,y,z:ℝ.  ((y < r0) ⇒ (x < z ⇐⇒ (z * y) < (x * y)))
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{}.    ((y  <  r0)  {}\mRightarrow{}  (x  <  z  \mLeftarrow{}{}\mRightarrow{}  (z  *  y)  <  (x  *  y)))


By

---

Latex:
Auto

---

Home Index