---

Step * of Lemma rmul_preserves_rneq_iff

∀a,b,x:ℝ.  (x ≠ r0 ⇒ (a ≠ b ⇐⇒ x * a ≠ x * b))
BY
{ Auto }

1
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. x ≠ r0
5. a ≠ b
⊢ x * a ≠ x * b

2
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. x ≠ r0
5. x * a ≠ x * b
⊢ a ≠ b

---

Latex:

---

Latex:
\mforall{}a,b,x:\mBbbR{}.    (x  \mneq{}  r0  {}\mRightarrow{}  (a  \mneq{}  b  \mLeftarrow{}{}\mRightarrow{}  x  *  a  \mneq{}  x  *  b))


By

---

Latex:
Auto

---

Home Index