Metamath Proof Explorer

Theorem xnegre

Description: An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion xnegre 
|- ( A e. RR* -> ( A e. RR <-> -e A e. RR ) )

Proof

Step Hyp Ref Expression
1 xnegrecl 
 |-  ( A e. RR -> -e A e. RR )
2 1 adantl 
 |-  ( ( A e. RR* /\ A e. RR ) -> -e A e. RR )
3 xnegrecl2 
 |-  ( ( A e. RR* /\ -e A e. RR ) -> A e. RR )
4 2 3 impbida 
 |-  ( A e. RR* -> ( A e. RR <-> -e A e. RR ) )