Description: Distribution of negative over addition. (Contributed by NM, 1-Jan-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | negdi2 | |- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A - B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negdi | |- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A + -u B ) ) |
|
2 | negcl | |- ( A e. CC -> -u A e. CC ) |
|
3 | negsub | |- ( ( -u A e. CC /\ B e. CC ) -> ( -u A + -u B ) = ( -u A - B ) ) |
|
4 | 2 3 | sylan | |- ( ( A e. CC /\ B e. CC ) -> ( -u A + -u B ) = ( -u A - B ) ) |
5 | 1 4 | eqtrd | |- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A - B ) ) |