Description: 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | xrltne | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐵 ≠ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc | ⊢ ( 𝐴 < 𝐵 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) | |
2 | xrltso | ⊢ < Or ℝ* | |
3 | sotrieq | ⊢ ( ( < Or ℝ* ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) ) | |
4 | 2 3 | mpan | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
5 | 4 | necon2abid | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ↔ 𝐴 ≠ 𝐵 ) ) |
6 | 1 5 | syl5ib | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 ≠ 𝐵 ) ) |
7 | 6 | 3impia | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐴 ≠ 𝐵 ) |
8 | 7 | necomd | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐵 ≠ 𝐴 ) |