Metamath Proof Explorer

Theorem letric

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

Ref Expression
Assertion letric ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∨ B ≤ A

Proof

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