Theorem xrltnle

Description: "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		xrlenlt	|- ( ( B e. RR* /\ A e. RR* ) -> ( B <_ A <-> -. A < B ) )
2	1	con2bid	|- ( ( B e. RR* /\ A e. RR* ) -> ( A < B <-> -. B <_ A ) )
3	2	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )