This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xltneg

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

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

Proof

Step Hyp Ref Expression
1 xltnegi 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> -e B < -e A )
2 1 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> -e B < -e A ) )
3 xnegcl 
 |-  ( B e. RR* -> -e B e. RR* )
4 xnegcl 
 |-  ( A e. RR* -> -e A e. RR* )
5 xltnegi 
 |-  ( ( -e B e. RR* /\ -e A e. RR* /\ -e B < -e A ) -> -e -e A < -e -e B )
6 5 3expia 
 |-  ( ( -e B e. RR* /\ -e A e. RR* ) -> ( -e B < -e A -> -e -e A < -e -e B ) )
7 3 4 6 syl2anr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e B < -e A -> -e -e A < -e -e B ) )
8 xnegneg 
 |-  ( A e. RR* -> -e -e A = A )
9 xnegneg 
 |-  ( B e. RR* -> -e -e B = B )
10 8 9 breqan12d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e -e A < -e -e B <-> A < B ) )
11 7 10 sylibd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e B < -e A -> A < B ) )
12 2 11 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -e B < -e A ) )