Theorem renegid

Description: Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	renegid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 0 −ℝ 𝐴 ) = ( 0 −ℝ 𝐴 )
2		rernegcl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
3		renegadd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℝ ) → ( ( 0 −ℝ 𝐴 ) = ( 0 −ℝ 𝐴 ) ↔ ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 ) )
4	2 3	mpdan	⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 𝐴 ) = ( 0 −ℝ 𝐴 ) ↔ ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 ) )
5	1 4	mpbii	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 )