Theorem xrletri

Description: Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		xrltnle	|- ( ( B e. RR* /\ A e. RR* ) -> ( B < A <-> -. A <_ B ) )
2	1	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( B < A <-> -. A <_ B ) )
3		xrltle	|- ( ( B e. RR* /\ A e. RR* ) -> ( B < A -> B <_ A ) )
4	3	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( B < A -> B <_ A ) )
5	2 4	sylbird	|- ( ( A e. RR* /\ B e. RR* ) -> ( -. A <_ B -> B <_ A ) )
6	5	orrd	|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B \/ B <_ A ) )