Metamath Proof Explorer

Theorem xmulneg2

Description: Extended real version of mulneg2 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulneg2 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A *e -e B ) = -e ( A *e B ) )

Proof

Step Hyp Ref Expression
1 xmulneg1 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( -e B *e A ) = -e ( B *e A ) )
2 1 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e B *e A ) = -e ( B *e A ) )
3 xnegcl 
 |-  ( B e. RR* -> -e B e. RR* )
4 xmulcom 
 |-  ( ( A e. RR* /\ -e B e. RR* ) -> ( A *e -e B ) = ( -e B *e A ) )
5 3 4 sylan2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e -e B ) = ( -e B *e A ) )
6 xmulcom 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = ( B *e A ) )
7 xnegeq 
 |-  ( ( A *e B ) = ( B *e A ) -> -e ( A *e B ) = -e ( B *e A ) )
8 6 7 syl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> -e ( A *e B ) = -e ( B *e A ) )
9 2 5 8 3eqtr4d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e -e B ) = -e ( A *e B ) )