Description: Multiplication by 0 . Theorem I.6 of Apostol p. 18. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

Hypothesis  muld.1   ( ph > A e. CC ) 

Assertion  mul01d   ( ph > ( A x. 0 ) = 0 ) 
Step  Hyp  Ref  Expression 

1  muld.1   ( ph > A e. CC ) 

2  mul01   ( A e. CC > ( A x. 0 ) = 0 ) 

3  1 2  syl   ( ph > ( A x. 0 ) = 0 ) 