Metamath Proof Explorer


Theorem negsubdii

Description: Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999)

Ref Expression
Hypotheses negidi.1
|- A e. CC
pncan3i.2
|- B e. CC
Assertion negsubdii
|- -u ( A - B ) = ( -u A + B )

Proof

Step Hyp Ref Expression
1 negidi.1
 |-  A e. CC
2 pncan3i.2
 |-  B e. CC
3 2 negcli
 |-  -u B e. CC
4 1 3 negdii
 |-  -u ( A + -u B ) = ( -u A + -u -u B )
5 1 2 negsubi
 |-  ( A + -u B ) = ( A - B )
6 5 negeqi
 |-  -u ( A + -u B ) = -u ( A - B )
7 2 negnegi
 |-  -u -u B = B
8 7 oveq2i
 |-  ( -u A + -u -u B ) = ( -u A + B )
9 4 6 8 3eqtr3i
 |-  -u ( A - B ) = ( -u A + B )