Metamath Proof Explorer


Theorem xlt0neg1

Description: Extended real version of lt0neg1 . (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

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