Metamath Proof Explorer

Theorem xlenegcon1

Description: Extended real version of lenegcon1 . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Assertion xlenegcon1 
|- ( ( A e. RR* /\ B e. RR* ) -> ( -e A <_ B <-> -e B <_ A ) )

Proof

Step Hyp Ref Expression
1 xnegcl 
 |-  ( A e. RR* -> -e A e. RR* )
2 xleneg 
 |-  ( ( -e A e. RR* /\ B e. RR* ) -> ( -e A <_ B <-> -e B <_ -e -e A ) )
3 1 2 sylan 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A <_ B <-> -e B <_ -e -e A ) )
4 xnegneg 
 |-  ( A e. RR* -> -e -e A = A )
5 4 breq2d 
 |-  ( A e. RR* -> ( -e B <_ -e -e A <-> -e B <_ A ) )
6 5 adantr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e B <_ -e -e A <-> -e B <_ A ) )
7 3 6 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A <_ B <-> -e B <_ A ) )