---

Step * of Lemma mul-zero

∀[x:ℤ]. (x * 0 ~ 0)
BY
{ ((UnivCD THENA Auto) THEN (RWO "mul-commutes" 0 THENA Auto) THEN BLemma `zero-mul` THEN Declaration) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (x  *  0  \msim{}  0)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "mul-commutes"  0  THENA  Auto)  THEN  BLemma  `zero-mul`  THEN  Declaration)

---

Home Index