Theorem negsubdi3d

Description: Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	negsubdi3d.1	|- ( ph -> A e. CC )
	negsubdi3d.2	|- ( ph -> B e. CC )
Assertion	negsubdi3d	|- ( ph -> -u ( A - B ) = ( -u A - -u B ) )

Proof

Step	Hyp	Ref	Expression
1		negsubdi3d.1	|- ( ph -> A e. CC )
2		negsubdi3d.2	|- ( ph -> B e. CC )
3	1 2	negsubdi2d	|- ( ph -> -u ( A - B ) = ( B - A ) )
4	1 2	neg2subd	|- ( ph -> ( -u A - -u B ) = ( B - A ) )
5	3 4	eqtr4d	|- ( ph -> -u ( A - B ) = ( -u A - -u B ) )