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 )