Metamath Proof Explorer

Theorem sqmul

Description: Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008)

Ref Expression
Assertion sqmul 
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ 2 ) = ( ( A ^ 2 ) x. ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 mulexp 
 |-  ( ( A e. CC /\ B e. CC /\ 2 e. NN0 ) -> ( ( A x. B ) ^ 2 ) = ( ( A ^ 2 ) x. ( B ^ 2 ) ) )
3 1 2 mp3an3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ 2 ) = ( ( A ^ 2 ) x. ( B ^ 2 ) ) )