Metamath Proof Explorer

Theorem letri3

Description: Trichotomy law. (Contributed by NM, 14-May-1999)

Ref Expression
Assertion letri3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ B ≤ A

Proof

Step Hyp Ref Expression
1 lttri3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ ¬ A < B ∧ ¬ B < A
2 1 biancomd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ ¬ B < A ∧ ¬ A < B
3 lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
4 lenlt ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ↔ ¬ A < B
5 4 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ↔ ¬ A < B
6 3 5 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∧ B ≤ A ↔ ¬ B < A ∧ ¬ A < B
7 2 6 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ B ≤ A