# Metamath Proof Explorer

## Theorem xrltne

Description: 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006)

Ref Expression
Assertion xrltne ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\to {B}\ne {A}$

### Proof

Step Hyp Ref Expression
1 orc ${⊢}{A}<{B}\to \left({A}<{B}\vee {B}<{A}\right)$
2 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
3 sotrieq ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\right)\to \left({A}={B}↔¬\left({A}<{B}\vee {B}<{A}\right)\right)$
4 2 3 mpan ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}={B}↔¬\left({A}<{B}\vee {B}<{A}\right)\right)$
5 4 necon2abid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A}<{B}\vee {B}<{A}\right)↔{A}\ne {B}\right)$
6 1 5 syl5ib ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to {A}\ne {B}\right)$
7 6 3impia ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\to {A}\ne {B}$
8 7 necomd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\to {B}\ne {A}$