Theorem renegid

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

	Ref	Expression
Assertion	renegid	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢0{-}_{ℝ}A=0{-}_{ℝ}A$$
2		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
3		renegadd	$$⊢\left(A\in ℝ\wedge 0{-}_{ℝ}A\in ℝ\right)\to \left(0{-}_{ℝ}A=0{-}_{ℝ}A\leftrightarrow A+\left(0{-}_{ℝ}A\right)=0\right)$$
4	2 3	mpdan	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A=0{-}_{ℝ}A\leftrightarrow A+\left(0{-}_{ℝ}A\right)=0\right)$$
5	1 4	mpbii	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)=0$$