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 ) ) |
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 ) ) |