Metamath Proof Explorer

Theorem negreb

Description: The negative of a real is real. (Contributed by NM, 11-Aug-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion negreb 
|- ( A e. CC -> ( -u A e. RR <-> A e. RR ) )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( -u A e. RR -> -u -u A e. RR )
2 negneg 
 |-  ( A e. CC -> -u -u A = A )
3 2 eleq1d 
 |-  ( A e. CC -> ( -u -u A e. RR <-> A e. RR ) )
4 1 3 imbitrid 
 |-  ( A e. CC -> ( -u A e. RR -> A e. RR ) )
5 renegcl 
 |-  ( A e. RR -> -u A e. RR )
6 4 5 impbid1 
 |-  ( A e. CC -> ( -u A e. RR <-> A e. RR ) )