---

Step * of Lemma zero_ann_a

∀[a,b:ℤ].  (a * b) = 0 ∈ ℤ supposing (a = 0 ∈ ℤ) ∨ (b = 0 ∈ ℤ)
BY
{ (((UnivCD THENM D (-1)) THENA Auto) THEN HypSubst 3 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].    (a  *  b)  =  0  supposing  (a  =  0)  \mvee{}  (b  =  0)


By

---

Latex:
(((UnivCD  THENM  D  (-1))  THENA  Auto)  THEN  HypSubst  3  0\mcdot{}  THEN  Auto)

---

Home Index