---

Step * of Lemma rmul_preserves_rless

∀x,y,z:ℝ.  ((r0 < y) ⇒ (x < z ⇐⇒ (x * y) < (z * y)))
BY
{ Auto }

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

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

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbR{}.    ((r0  <  y)  {}\mRightarrow{}  (x  <  z  \mLeftarrow{}{}\mRightarrow{}  (x  *  y)  <  (z  *  y)))


By

---

Latex:
Auto

---

Home Index