Metamath Proof Explorer

Theorem negelrp

Description: Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018)

Ref Expression
Assertion negelrp 
|- ( A e. RR -> ( -u A e. RR+ <-> A < 0 ) )

Proof

Step Hyp Ref Expression
1 elrp 
 |-  ( -u A e. RR+ <-> ( -u A e. RR /\ 0 < -u A ) )
2 lt0neg1 
 |-  ( A e. RR -> ( A < 0 <-> 0 < -u A ) )
3 renegcl 
 |-  ( A e. RR -> -u A e. RR )
4 3 biantrurd 
 |-  ( A e. RR -> ( 0 < -u A <-> ( -u A e. RR /\ 0 < -u A ) ) )
5 2 4 bitr2d 
 |-  ( A e. RR -> ( ( -u A e. RR /\ 0 < -u A ) <-> A < 0 ) )
6 1 5 syl5bb 
 |-  ( A e. RR -> ( -u A e. RR+ <-> A < 0 ) )