Metamath Proof Explorer


Theorem neg2sub

Description: Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 negcl
 |-  ( A e. CC -> -u A e. CC )
2 subneg
 |-  ( ( -u A e. CC /\ B e. CC ) -> ( -u A - -u B ) = ( -u A + B ) )
3 1 2 sylan
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A - -u B ) = ( -u A + B ) )
4 negsubdi
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( -u A + B ) )
5 negsubdi2
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
6 3 4 5 3eqtr2d
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A - -u B ) = ( B - A ) )