This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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