Step * 1 of Lemma mul-commutes

.....assertion..... 
x,y:ℤ.  ((x y) (y x) ∈ ℤ)
BY
TACTIC:((UnivCD THENA Auto) THEN Refine_multiplyCommutative THEN Fold `member` THEN Declaration) }


Latex:


Latex:
.....assertion..... 
\mforall{}x,y:\mBbbZ{}.    ((x  *  y)  =  (y  *  x))


By


Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  Refine\_multiplyCommutative  THEN  Fold  `member`  0  THEN  Declaration)




Home Index