Theorem leltne

Description: 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999)

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

Proof

Step	Hyp	Ref	Expression
1		lttri3	|- ( ( 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		leloe	|- ( ( 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 ) )