Metamath Proof Explorer

Theorem xrleltne

Description: 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 xrlttri3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ ¬ A < B ∧ ¬ B < A
2 simpl ⊢ ¬ A < B ∧ ¬ B < A → ¬ A < B
3 1 2 biimtrdi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B → ¬ A < B
4 3 adantr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A = B → ¬ A < B
5 xrleloe ⊢ 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