Metamath Proof Explorer

Theorem negrebi

Description: The negative of a real is real. (Contributed by NM, 11-Aug-1999)

Ref Expression
Hypothesis negidi.1 
|- A e. CC
Assertion negrebi 
|- ( -u A e. RR <-> A e. RR )

Proof

Step Hyp Ref Expression
1 negidi.1 
 |-  A e. CC
2 negreb 
 |-  ( A e. CC -> ( -u A e. RR <-> A e. RR ) )
3 1 2 ax-mp 
 |-  ( -u A e. RR <-> A e. RR )