Metamath Proof Explorer

Theorem mulneg1

Description: Product with negative is negative of product. Theorem I.12 of Apostol p. 18. (Contributed by NM, 14-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion mulneg1 
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. B ) = -u ( A x. B ) )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 subdir 
 |-  ( ( 0 e. CC /\ A e. CC /\ B e. CC ) -> ( ( 0 - A ) x. B ) = ( ( 0 x. B ) - ( A x. B ) ) )
3 1 2 mp3an1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 0 - A ) x. B ) = ( ( 0 x. B ) - ( A x. B ) ) )
4 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
5 4 mul02d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 0 x. B ) = 0 )
6 5 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 0 x. B ) - ( A x. B ) ) = ( 0 - ( A x. B ) ) )
7 3 6 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 0 - A ) x. B ) = ( 0 - ( A x. B ) ) )
8 df-neg 
 |-  -u A = ( 0 - A )
9 8 oveq1i 
 |-  ( -u A x. B ) = ( ( 0 - A ) x. B )
10 df-neg 
 |-  -u ( A x. B ) = ( 0 - ( A x. B ) )
11 7 9 10 3eqtr4g 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A x. B ) = -u ( A x. B ) )