Metamath Proof Explorer

Theorem xle0neg2

Description: Extended real version of le0neg2 . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion xle0neg2 
|- ( A e. RR* -> ( 0 <_ A <-> -e A <_ 0 ) )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 xleneg 
 |-  ( ( 0 e. RR* /\ A e. RR* ) -> ( 0 <_ A <-> -e A <_ -e 0 ) )
3 1 2 mpan 
 |-  ( A e. RR* -> ( 0 <_ A <-> -e A <_ -e 0 ) )
4 xneg0 
 |-  -e 0 = 0
5 4 breq2i 
 |-  ( -e A <_ -e 0 <-> -e A <_ 0 )
6 3 5 bitrdi 
 |-  ( A e. RR* -> ( 0 <_ A <-> -e A <_ 0 ) )