This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. RR* /\ B e. RR* /\ A < B ) -> B =/= A )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( A < B -> ( A < B \/ B < A ) )
2 xrltso 
 |-  < Or RR*
3 sotrieq 
 |-  ( ( < Or RR* /\ ( A e. RR* /\ B e. RR* ) ) -> ( A = B <-> -. ( A < B \/ B < A ) ) )
4 2 3 mpan 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> -. ( A < B \/ B < A ) ) )
5 4 necon2abid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A < B \/ B < A ) <-> A =/= B ) )
6 1 5 imbitrid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> A =/= B ) )
7 6 3impia 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A =/= B )
8 7 necomd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B =/= A )