Theorem letric

Description: Trichotomy law. (Contributed by NM, 18-Aug-1999) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

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