Metamath Proof Explorer

Theorem leltne

Description: 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999)

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

Proof

Step Hyp Ref Expression
1 lttri3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ ¬ A < B ∧ ¬ B < A
2 simpl ⊢ ¬ A < B ∧ ¬ B < A → ¬ A < B
3 1 2 syl6bi ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B → ¬ A < B
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A = B → ¬ A < B
5 leloe ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A < B ∨ A = B
6 5 biimpa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A < B ∨ A = B
7 6 ord ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → ¬ A < B → A = B
8 4 7 impbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A = B ↔ ¬ A < B
9 8 necon2abid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A < B ↔ A ≠ B
10 necom ⊢ B ≠ A ↔ A ≠ B
11 9 10 bitr4di ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A < B ↔ B ≠ A
12 11 3impa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A < B ↔ B ≠ A