Theorem xrletri

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

	Ref	Expression
Assertion	xrletri	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\vee B\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrltnle	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B<A\leftrightarrow \neg A\le B\right)$$
2	1	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B<A\leftrightarrow \neg A\le B\right)$$
3		xrltle	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B<A\to B\le A\right)$$
4	3	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B<A\to B\le A\right)$$
5	2 4	sylbird	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\neg A\le B\to B\le A\right)$$
6	5	orrd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\vee B\le A\right)$$