Theorem subneg

Description: Relationship between subtraction and negative. (Contributed by NM, 10-May-2004) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	subneg	|- ( ( A e. CC /\ B e. CC ) -> ( A - -u B ) = ( A + B ) )

Proof

Step	Hyp	Ref	Expression
1		df-neg	|- -u B = ( 0 - B )
2	1	oveq2i	|- ( A - -u B ) = ( A - ( 0 - B ) )
3		0cn	|- 0 e. CC
4		subsub	|- ( ( A e. CC /\ 0 e. CC /\ B e. CC ) -> ( A - ( 0 - B ) ) = ( ( A - 0 ) + B ) )
5	3 4	mp3an2	|- ( ( A e. CC /\ B e. CC ) -> ( A - ( 0 - B ) ) = ( ( A - 0 ) + B ) )
6	2 5	syl5eq	|- ( ( A e. CC /\ B e. CC ) -> ( A - -u B ) = ( ( A - 0 ) + B ) )
7		subid1	|- ( A e. CC -> ( A - 0 ) = A )
8	7	adantr	|- ( ( A e. CC /\ B e. CC ) -> ( A - 0 ) = A )
9	8	oveq1d	|- ( ( A e. CC /\ B e. CC ) -> ( ( A - 0 ) + B ) = ( A + B ) )
10	6 9	eqtrd	|- ( ( A e. CC /\ B e. CC ) -> ( A - -u B ) = ( A + B ) )