Metamath Proof Explorer

Theorem negsubdi

Description: Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 subsub 
 |-  ( ( 0 e. CC /\ A e. CC /\ B e. CC ) -> ( 0 - ( A - B ) ) = ( ( 0 - A ) + B ) )
3 1 2 mp3an1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 0 - ( A - B ) ) = ( ( 0 - A ) + B ) )
4 df-neg 
 |-  -u ( A - B ) = ( 0 - ( A - B ) )
5 df-neg 
 |-  -u A = ( 0 - A )
6 5 oveq1i 
 |-  ( -u A + B ) = ( ( 0 - A ) + B )
7 3 4 6 3eqtr4g 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( -u A + B ) )