Metamath Proof Explorer

Theorem ltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999)

Ref Expression
Assertion ltlen ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A ≤ B ∧ B ≠ A

Proof

Step Hyp Ref Expression
1 ltle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → A ≤ B
2 ltne ⊢ A ∈ ℝ ∧ A < B → B ≠ A
3 2 ex ⊢ A ∈ ℝ → A < B → B ≠ A
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → B ≠ A
5 1 4 jcad ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → A ≤ B ∧ B ≠ A
6 leloe ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A < B ∨ A = B
7 df-ne ⊢ B ≠ A ↔ ¬ B = A
8 pm2.24 ⊢ B = A → ¬ B = A → A < B
9 8 eqcoms ⊢ A = B → ¬ B = A → A < B
10 7 9 biimtrid ⊢ A = B → B ≠ A → A < B
11 10 jao1i ⊢ A < B ∨ A = B → B ≠ A → A < B
12 6 11 biimtrdi ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B → B ≠ A → A < B
13 12 impd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∧ B ≠ A → A < B
14 5 13 impbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A ≤ B ∧ B ≠ A