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	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rernegcl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
2		rernegcl	⊢ ( ( 0 −ℝ 𝐴 ) ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ∈ ℝ )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ∈ ℝ )
4		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
5		renegid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 )
6		elre0re	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
7	5 6	eqeltrd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 0 −ℝ 𝐴 ) ) ∈ ℝ )
8		readdid1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 0 ) = 𝐴 )
9		repncan3	⊢ ( ( ( 0 −ℝ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) = 0 )
10	1 6 9	syl2anc	⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) = 0 )
11	10	oveq2d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) ) = ( 𝐴 + 0 ) )
12		readdid2	⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 )
13	8 11 12	3eqtr4d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) ) = ( 0 + 𝐴 ) )
14		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
15	1	recnd	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℂ )
16	3	recnd	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ∈ ℂ )
17	14 15 16	addassd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) = ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) ) )
18	5	oveq1d	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) = ( 0 + 𝐴 ) )
19	13 17 18	3eqtr4d	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) = ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) )
20		readdcan	⊢ ( ( ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐴 + ( 0 −ℝ 𝐴 ) ) ∈ ℝ ) → ( ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) = ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) ↔ ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) = 𝐴 ) )
21	20	biimpa	⊢ ( ( ( ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐴 + ( 0 −ℝ 𝐴 ) ) ∈ ℝ ) ∧ ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) ) = ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) ) → ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) = 𝐴 )
22	3 4 7 19 21	syl31anc	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 𝐴 ) ) = 𝐴 )