---

Step * of Lemma absval_eq

∀x,y:ℤ.  (|x| = |y| ∈ ℤ ⇐⇒ x = ± y)
BY
{ (((UnivCD THENA Auto) THEN Unfold `pm_equal` 0) THEN RWO "absval_unfold" 0 THEN Repeat (AutoSplit) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    (|x|  =  |y|  \mLeftarrow{}{}\mRightarrow{}  x  =  \mpm{}  y)


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `pm\_equal`  0)
  THEN  RWO  "absval\_unfold"  0
  THEN  Repeat  (AutoSplit)
  THEN  Auto')

---

Home Index