---

Step * of Lemma rabs-rneq

No Annotations
∀a,b:ℝ.  (|a| ≠ |b| ⇒ a ≠ b)
BY
{ (Auto
   THEN D -1
   THEN (RWO  "rabs-strict-ub" (-1) THENA Auto)
   THEN RWO "rabs-rless-iff" (-1)
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbR{}.    (|a|  \mneq{}  |b|  {}\mRightarrow{}  a  \mneq{}  b)


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (RWO    "rabs-strict-ub"  (-1)  THENA  Auto)
  THEN  RWO  "rabs-rless-iff"  (-1)
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index