Metamath Proof Explorer

Theorem renegid2

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

Ref Expression
Assertion renegid2 
|- ( A e. RR -> ( ( 0 -R A ) + A ) = 0 )

Proof

Step Hyp Ref Expression
1 renegid 
 |-  ( A e. RR -> ( A + ( 0 -R A ) ) = 0 )
2 1 oveq2d 
 |-  ( A e. RR -> ( ( 0 -R A ) + ( A + ( 0 -R A ) ) ) = ( ( 0 -R A ) + 0 ) )
3 rernegcl 
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
4 readdid1 
 |-  ( ( 0 -R A ) e. RR -> ( ( 0 -R A ) + 0 ) = ( 0 -R A ) )
5 3 4 syl 
 |-  ( A e. RR -> ( ( 0 -R A ) + 0 ) = ( 0 -R A ) )
6 2 5 eqtrd 
 |-  ( A e. RR -> ( ( 0 -R A ) + ( A + ( 0 -R A ) ) ) = ( 0 -R A ) )
7 3 recnd 
 |-  ( A e. RR -> ( 0 -R A ) e. CC )
8 recn 
 |-  ( A e. RR -> A e. CC )
9 7 8 7 addassd 
 |-  ( A e. RR -> ( ( ( 0 -R A ) + A ) + ( 0 -R A ) ) = ( ( 0 -R A ) + ( A + ( 0 -R A ) ) ) )
10 readdid2 
 |-  ( ( 0 -R A ) e. RR -> ( 0 + ( 0 -R A ) ) = ( 0 -R A ) )
11 3 10 syl 
 |-  ( A e. RR -> ( 0 + ( 0 -R A ) ) = ( 0 -R A ) )
12 6 9 11 3eqtr4d 
 |-  ( A e. RR -> ( ( ( 0 -R A ) + A ) + ( 0 -R A ) ) = ( 0 + ( 0 -R A ) ) )
13 id 
 |-  ( A e. RR -> A e. RR )
14 3 13 readdcld 
 |-  ( A e. RR -> ( ( 0 -R A ) + A ) e. RR )
15 elre0re 
 |-  ( A e. RR -> 0 e. RR )
16 readdcan2 
 |-  ( ( ( ( 0 -R A ) + A ) e. RR /\ 0 e. RR /\ ( 0 -R A ) e. RR ) -> ( ( ( ( 0 -R A ) + A ) + ( 0 -R A ) ) = ( 0 + ( 0 -R A ) ) <-> ( ( 0 -R A ) + A ) = 0 ) )
17 14 15 3 16 syl3anc 
 |-  ( A e. RR -> ( ( ( ( 0 -R A ) + A ) + ( 0 -R A ) ) = ( 0 + ( 0 -R A ) ) <-> ( ( 0 -R A ) + A ) = 0 ) )
18 12 17 mpbid 
 |-  ( A e. RR -> ( ( 0 -R A ) + A ) = 0 )