---

Step * of Lemma mul_nzero

∀[a,b:ℤ-o].  a * b ≠ 0
BY
{ (Auto THEN InstLemma `mul_wf_nzero` [⌜a⌝;⌜b⌝]⋅ THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}\msupminus{}\msupzero{}].    a  *  b  \mneq{}  0


By

---

Latex:
(Auto  THEN  InstLemma  `mul\_wf\_nzero`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index