Description: Absolute value distributes over multiplication. Proposition 103.7(f) of Gleason p. 133. (Contributed by Mario Carneiro, 29May2016)
Ref  Expression  

Hypotheses  abscld.1   ( ph > A e. CC ) 

abssubd.2   ( ph > B e. CC ) 

Assertion  absmuld   ( ph > ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) ) 
Step  Hyp  Ref  Expression 

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

2  abssubd.2   ( ph > B e. CC ) 

3  absmul   ( ( A e. CC /\ B e. CC ) > ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) ) 

4  1 2 3  syl2anc   ( ph > ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) ) 