Theorem renegneg

Description: A real number is equal to the negative of its negative. Compare negneg . (Contributed by SN, 13-Feb-2024)

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

Proof

Step	Hyp	Ref	Expression
1		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
2		rernegcl	$$⊢0{-}_{ℝ}A\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\in ℝ$$
3	1 2	syl	$$⊢A\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\in ℝ$$
4		id	$$⊢A\in ℝ\to A\in ℝ$$
5		renegid	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)=0$$
6		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
7	5 6	eqeltrd	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)\in ℝ$$
8		readdid1	$$⊢A\in ℝ\to A+0=A$$
9		repncan3	$$⊢\left(0{-}_{ℝ}A\in ℝ\wedge 0\in ℝ\right)\to \left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=0$$
10	1 6 9	syl2anc	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=0$$
11	10	oveq2d	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=A+0$$
12		readdid2	$$⊢A\in ℝ\to 0+A=A$$
13	8 11 12	3eqtr4d	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=0+A$$
14		recn	$$⊢A\in ℝ\to A\in ℂ$$
15	1	recnd	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℂ$$
16	3	recnd	$$⊢A\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\in ℂ$$
17	14 15 16	addassd	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)$$
18	5	oveq1d	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)+A=0+A$$
19	13 17 18	3eqtr4d	$$⊢A\in ℝ\to A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=A+\left(0{-}_{ℝ}A\right)+A$$
20		readdcan	$$⊢\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\in ℝ\wedge A\in ℝ\wedge A+\left(0{-}_{ℝ}A\right)\in ℝ\right)\to \left(A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=A+\left(0{-}_{ℝ}A\right)+A\leftrightarrow 0{-}_{ℝ}\left(0{-}_{ℝ}A\right)=A\right)$$
21	20	biimpa	$$⊢\left(\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\in ℝ\wedge A\in ℝ\wedge A+\left(0{-}_{ℝ}A\right)\in ℝ\right)\wedge A+\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}\left(0{-}_{ℝ}A\right)\right)=A+\left(0{-}_{ℝ}A\right)+A\right)\to 0{-}_{ℝ}\left(0{-}_{ℝ}A\right)=A$$
22	3 4 7 19 21	syl31anc	$$⊢A\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}A\right)=A$$