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	syl5ib	|- ( ( 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 )