Metamath Proof Explorer


Theorem xrltne

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

Ref Expression
Assertion xrltne A * B * A < B B A

Proof

Step Hyp Ref Expression
1 orc A < B A < B B < A
2 xrltso < Or *
3 sotrieq < Or * A * B * A = B ¬ A < B B < A
4 2 3 mpan A * B * A = B ¬ A < B B < A
5 4 necon2abid A * B * A < B B < A A B
6 1 5 syl5ib A * B * A < B A B
7 6 3impia A * B * A < B A B
8 7 necomd A * B * A < B B A