Metamath Proof Explorer

Theorem xnegrecl2

Description: If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion xnegrecl2 
|- ( ( A e. RR* /\ -e A e. RR ) -> A e. RR )

Proof

Step Hyp Ref Expression
1 xnegneg 
 |-  ( A e. RR* -> -e -e A = A )
2 1 adantr 
 |-  ( ( A e. RR* /\ -e A e. RR ) -> -e -e A = A )
3 xnegrecl 
 |-  ( -e A e. RR -> -e -e A e. RR )
4 3 adantl 
 |-  ( ( A e. RR* /\ -e A e. RR ) -> -e -e A e. RR )
5 2 4 eqeltrrd 
 |-  ( ( A e. RR* /\ -e A e. RR ) -> A e. RR )