Metamath Proof Explorer

Theorem ltnltne

Description: Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Assertion ltnltne ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ B < A ∧ ¬ B = A

Proof

Step Hyp Ref Expression
1 ltnle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ B ≤ A
2 leloe ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ↔ B < A ∨ B = A
3 2 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ↔ B < A ∨ B = A
4 3 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B ≤ A ↔ ¬ B < A ∨ B = A
5 ioran ⊢ ¬ B < A ∨ B = A ↔ ¬ B < A ∧ ¬ B = A
6 5 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B < A ∨ B = A ↔ ¬ B < A ∧ ¬ B = A
7 1 4 6 3bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ B < A ∧ ¬ B = A