Metamath Proof Explorer

Theorem resubeulem1

Description: Lemma for resubeu . A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 elre0re 
 |-  ( A e. RR -> 0 e. RR )
2 1 recnd 
 |-  ( A e. RR -> 0 e. CC )
3 1 1 readdcld 
 |-  ( A e. RR -> ( 0 + 0 ) e. RR )
4 rernegcl 
 |-  ( ( 0 + 0 ) e. RR -> ( 0 -R ( 0 + 0 ) ) e. RR )
5 3 4 syl 
 |-  ( A e. RR -> ( 0 -R ( 0 + 0 ) ) e. RR )
6 5 recnd 
 |-  ( A e. RR -> ( 0 -R ( 0 + 0 ) ) e. CC )
7 2 2 6 addassd 
 |-  ( A e. RR -> ( ( 0 + 0 ) + ( 0 -R ( 0 + 0 ) ) ) = ( 0 + ( 0 + ( 0 -R ( 0 + 0 ) ) ) ) )
8 renegid 
 |-  ( ( 0 + 0 ) e. RR -> ( ( 0 + 0 ) + ( 0 -R ( 0 + 0 ) ) ) = 0 )
9 3 8 syl 
 |-  ( A e. RR -> ( ( 0 + 0 ) + ( 0 -R ( 0 + 0 ) ) ) = 0 )
10 7 9 eqtr3d 
 |-  ( A e. RR -> ( 0 + ( 0 + ( 0 -R ( 0 + 0 ) ) ) ) = 0 )
11 1 5 readdcld 
 |-  ( A e. RR -> ( 0 + ( 0 -R ( 0 + 0 ) ) ) e. RR )
12 renegadd 
 |-  ( ( 0 e. RR /\ ( 0 + ( 0 -R ( 0 + 0 ) ) ) e. RR ) -> ( ( 0 -R 0 ) = ( 0 + ( 0 -R ( 0 + 0 ) ) ) <-> ( 0 + ( 0 + ( 0 -R ( 0 + 0 ) ) ) ) = 0 ) )
13 1 11 12 syl2anc 
 |-  ( A e. RR -> ( ( 0 -R 0 ) = ( 0 + ( 0 -R ( 0 + 0 ) ) ) <-> ( 0 + ( 0 + ( 0 -R ( 0 + 0 ) ) ) ) = 0 ) )
14 10 13 mpbird 
 |-  ( A e. RR -> ( 0 -R 0 ) = ( 0 + ( 0 -R ( 0 + 0 ) ) ) )
15 14 eqcomd 
 |-  ( A e. RR -> ( 0 + ( 0 -R ( 0 + 0 ) ) ) = ( 0 -R 0 ) )