Theorem xrleltne

Description: 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006)

	Ref	Expression
Assertion	xrleltne	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A < B <-> B =/= A ) )

Proof

Step	Hyp	Ref	Expression
1		xrlttri3	|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
2		simpl	|- ( ( -. A < B /\ -. B < A ) -> -. A < B )
3	1 2	biimtrdi	|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B -> -. A < B ) )
4	3	adantr	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A = B -> -. A < B ) )
5		xrleloe	|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
6	5	biimpa	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A < B \/ A = B ) )
7	6	ord	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( -. A < B -> A = B ) )
8	4 7	impbid	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A = B <-> -. A < B ) )
9	8	necon2abid	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A < B <-> A =/= B ) )
10		necom	|- ( B =/= A <-> A =/= B )
11	9 10	bitr4di	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A < B <-> B =/= A ) )
12	11	3impa	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A < B <-> B =/= A ) )