Theorem negid

Description: Addition of a number and its negative. (Contributed by NM, 14-Mar-2005)

	Ref	Expression
Assertion	negid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
2	1	oveq2i	⊢ ( 𝐴 + - 𝐴 ) = ( 𝐴 + ( 0 − 𝐴 ) )
3		0cn	⊢ 0 ∈ ℂ
4		pncan3	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝐴 + ( 0 − 𝐴 ) ) = 0 )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( 0 − 𝐴 ) ) = 0 )
6	2 5	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )