Description: Multiplication by 0 . Theorem I.6 of Apostol p. 18. (Contributed by NM, 15May1999) (Revised by Scott Fenton, 3Jan2013)
Ref  Expression  

Assertion  mul01   ( A e. CC > ( A x. 0 ) = 0 ) 
Step  Hyp  Ref  Expression 

1  0cn   0 e. CC 

2  mulcom   ( ( A e. CC /\ 0 e. CC ) > ( A x. 0 ) = ( 0 x. A ) ) 

3  1 2  mpan2   ( A e. CC > ( A x. 0 ) = ( 0 x. A ) ) 
4  mul02   ( A e. CC > ( 0 x. A ) = 0 ) 

5  3 4  eqtrd   ( A e. CC > ( A x. 0 ) = 0 ) 