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 ) ) )