Step * of Lemma mul-zero

[x:ℤ]. (x 0)
BY
((UnivCD THENA Auto) THEN (RWO "mul-commutes" 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