---

Step * of Lemma rmul_preserves_rneq_iff2

∀a,b,x:ℝ.  (x ≠ r0 ⇒ (a ≠ b ⇐⇒ a * x ≠ b * x))
BY
{ (InstLemma `rmul_preserves_rneq_iff` []
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))
   THEN RWO "rmul_comm" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rmul\_preserves\_rneq\_iff`  []
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  RWO  "rmul\_comm"  0
  THEN  Auto)

---

Home Index