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 )