Theorem xrlelttric

Description: Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.1	|- ( -. B < A \/ B < A )
2		xrlenlt	|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
3	2	orbi1d	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A <_ B \/ B < A ) <-> ( -. B < A \/ B < A ) ) )
4	1 3	mpbiri	|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B \/ B < A ) )