Theorem renegid2

Description: Commuted version of renegid . (Contributed by SN, 4-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		renegid	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)=0$$
2	1	oveq2d	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)=\left(0{-}_{ℝ}A\right)+0$$
3		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
4		readdid1	$$⊢0{-}_{ℝ}A\in ℝ\to \left(0{-}_{ℝ}A\right)+0=0{-}_{ℝ}A$$
5	3 4	syl	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+0=0{-}_{ℝ}A$$
6	2 5	eqtrd	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)=0{-}_{ℝ}A$$
7	3	recnd	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℂ$$
8		recn	$$⊢A\in ℝ\to A\in ℂ$$
9	7 8 7	addassd	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)=\left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)$$
10		readdid2	$$⊢0{-}_{ℝ}A\in ℝ\to 0+\left(0{-}_{ℝ}A\right)=0{-}_{ℝ}A$$
11	3 10	syl	$$⊢A\in ℝ\to 0+\left(0{-}_{ℝ}A\right)=0{-}_{ℝ}A$$
12	6 9 11	3eqtr4d	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)=0+\left(0{-}_{ℝ}A\right)$$
13		id	$$⊢A\in ℝ\to A\in ℝ$$
14	3 13	readdcld	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A\in ℝ$$
15		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
16		readdcan2	$$⊢\left(\left(0{-}_{ℝ}A\right)+A\in ℝ\wedge 0\in ℝ\wedge 0{-}_{ℝ}A\in ℝ\right)\to \left(\left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)=0+\left(0{-}_{ℝ}A\right)\leftrightarrow \left(0{-}_{ℝ}A\right)+A=0\right)$$
17	14 15 3 16	syl3anc	$$⊢A\in ℝ\to \left(\left(0{-}_{ℝ}A\right)+A+\left(0{-}_{ℝ}A\right)=0+\left(0{-}_{ℝ}A\right)\leftrightarrow \left(0{-}_{ℝ}A\right)+A=0\right)$$
18	12 17	mpbid	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A=0$$