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

Metamath Proof Explorer

Theorem xposdif

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

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

Proof

Step Hyp Ref Expression
1 xnegcl 
 |-  ( B e. RR* -> -e B e. RR* )
2 xaddcl 
 |-  ( ( A e. RR* /\ -e B e. RR* ) -> ( A +e -e B ) e. RR* )
3 1 2 sylan2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e -e B ) e. RR* )
4 xlt0neg1 
 |-  ( ( A +e -e B ) e. RR* -> ( ( A +e -e B ) < 0 <-> 0 < -e ( A +e -e B ) ) )
5 3 4 syl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A +e -e B ) < 0 <-> 0 < -e ( A +e -e B ) ) )
6 xsubge0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
7 6 notbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. 0 <_ ( A +e -e B ) <-> -. B <_ A ) )
8 0xr 
 |-  0 e. RR*
9 xrltnle 
 |-  ( ( ( A +e -e B ) e. RR* /\ 0 e. RR* ) -> ( ( A +e -e B ) < 0 <-> -. 0 <_ ( A +e -e B ) ) )
10 3 8 9 sylancl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A +e -e B ) < 0 <-> -. 0 <_ ( A +e -e B ) ) )
11 xrltnle 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )
12 7 10 11 3bitr4d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A +e -e B ) < 0 <-> A < B ) )
13 xnegdi 
 |-  ( ( A e. RR* /\ -e B e. RR* ) -> -e ( A +e -e B ) = ( -e A +e -e -e B ) )
14 1 13 sylan2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> -e ( A +e -e B ) = ( -e A +e -e -e B ) )
15 xnegneg 
 |-  ( B e. RR* -> -e -e B = B )
16 15 oveq2d 
 |-  ( B e. RR* -> ( -e A +e -e -e B ) = ( -e A +e B ) )
17 16 adantl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A +e -e -e B ) = ( -e A +e B ) )
18 xnegcl 
 |-  ( A e. RR* -> -e A e. RR* )
19 xaddcom 
 |-  ( ( -e A e. RR* /\ B e. RR* ) -> ( -e A +e B ) = ( B +e -e A ) )
20 18 19 sylan 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A +e B ) = ( B +e -e A ) )
21 14 17 20 3eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> -e ( A +e -e B ) = ( B +e -e A ) )
22 21 breq2d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( 0 < -e ( A +e -e B ) <-> 0 < ( B +e -e A ) ) )
23 5 12 22 3bitr3d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> 0 < ( B +e -e A ) ) )