Theorem xrletri

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

	Ref	Expression
Assertion	xrletri	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xrltnle	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵 ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵 ) )
3		xrltle	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 < 𝐴 → 𝐵 ≤ 𝐴 ) )
4	3	ancoms	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < 𝐴 → 𝐵 ≤ 𝐴 ) )
5	2 4	sylbird	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐴 ≤ 𝐵 → 𝐵 ≤ 𝐴 ) )
6	5	orrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )