---

Step * of Lemma mul_wf_nzero

∀[a,b:ℤ-o].  (a * b ∈ ℤ-o)
BY
{ (Auto THEN D 0 THEN Auto THEN (FLemma `int_entire` [(-1)]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}\msupminus{}\msupzero{}].    (a  *  b  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{})


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  (FLemma  `int\_entire`  [(-1)])  THEN  Auto)

---

Home Index