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 
|- ( A e. RR -> ( 0 -R ( 0 -R A ) ) = A )

Proof

Step Hyp Ref Expression
1 rernegcl 
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
2 rernegcl 
 |-  ( ( 0 -R A ) e. RR -> ( 0 -R ( 0 -R A ) ) e. RR )
3 1 2 syl 
 |-  ( A e. RR -> ( 0 -R ( 0 -R A ) ) e. RR )
4 id 
 |-  ( A e. RR -> A e. RR )
5 renegid 
 |-  ( A e. RR -> ( A + ( 0 -R A ) ) = 0 )
6 elre0re 
 |-  ( A e. RR -> 0 e. RR )
7 5 6 eqeltrd 
 |-  ( A e. RR -> ( A + ( 0 -R A ) ) e. RR )
8 readdid1 
 |-  ( A e. RR -> ( A + 0 ) = A )
9 repncan3 
 |-  ( ( ( 0 -R A ) e. RR /\ 0 e. RR ) -> ( ( 0 -R A ) + ( 0 -R ( 0 -R A ) ) ) = 0 )
10 1 6 9 syl2anc 
 |-  ( A e. RR -> ( ( 0 -R A ) + ( 0 -R ( 0 -R A ) ) ) = 0 )
11 10 oveq2d 
 |-  ( A e. RR -> ( A + ( ( 0 -R A ) + ( 0 -R ( 0 -R A ) ) ) ) = ( A + 0 ) )
12 readdid2 
 |-  ( A e. RR -> ( 0 + A ) = A )
13 8 11 12 3eqtr4d 
 |-  ( A e. RR -> ( A + ( ( 0 -R A ) + ( 0 -R ( 0 -R A ) ) ) ) = ( 0 + A ) )
14 recn 
 |-  ( A e. RR -> A e. CC )
15 1 recnd 
 |-  ( A e. RR -> ( 0 -R A ) e. CC )
16 3 recnd 
 |-  ( A e. RR -> ( 0 -R ( 0 -R A ) ) e. CC )
17 14 15 16 addassd 
 |-  ( A e. RR -> ( ( A + ( 0 -R A ) ) + ( 0 -R ( 0 -R A ) ) ) = ( A + ( ( 0 -R A ) + ( 0 -R ( 0 -R A ) ) ) ) )
18 5 oveq1d 
 |-  ( A e. RR -> ( ( A + ( 0 -R A ) ) + A ) = ( 0 + A ) )
19 13 17 18 3eqtr4d 
 |-  ( A e. RR -> ( ( A + ( 0 -R A ) ) + ( 0 -R ( 0 -R A ) ) ) = ( ( A + ( 0 -R A ) ) + A ) )
20 readdcan 
 |-  ( ( ( 0 -R ( 0 -R A ) ) e. RR /\ A e. RR /\ ( A + ( 0 -R A ) ) e. RR ) -> ( ( ( A + ( 0 -R A ) ) + ( 0 -R ( 0 -R A ) ) ) = ( ( A + ( 0 -R A ) ) + A ) <-> ( 0 -R ( 0 -R A ) ) = A ) )
21 20 biimpa 
 |-  ( ( ( ( 0 -R ( 0 -R A ) ) e. RR /\ A e. RR /\ ( A + ( 0 -R A ) ) e. RR ) /\ ( ( A + ( 0 -R A ) ) + ( 0 -R ( 0 -R A ) ) ) = ( ( A + ( 0 -R A ) ) + A ) ) -> ( 0 -R ( 0 -R A ) ) = A )
22 3 4 7 19 21 syl31anc 
 |-  ( A e. RR -> ( 0 -R ( 0 -R A ) ) = A )