---

Step * of Lemma assoced_elim

∀a,b:ℤ.  (a ~ b ⇐⇒ (a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ))
BY
{ ((UnivCD THENM Unfolds ``assoced guard`` 0) THENA Auto) }

1
1. a : ℤ
2. b : ℤ
⊢ (a | b) ∧ (b | a) ⇐⇒ (a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (a  \msim{}  b  \mLeftarrow{}{}\mRightarrow{}  (a  =  b)  \mvee{}  (a  =  (-b)))


By

---

Latex:
((UnivCD  THENM  Unfolds  ``assoced  guard``  0)  THENA  Auto)

---

Home Index