Theorem ltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999)

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

Proof

Step	Hyp	Ref	Expression
1		ltle	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
2		ltne	|- ( ( A e. RR /\ A < B ) -> B =/= A )
3	2	ex	|- ( A e. RR -> ( A < B -> B =/= A ) )
4	3	adantr	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> B =/= A ) )
5	1 4	jcad	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> ( A <_ B /\ B =/= A ) ) )
6		leloe	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
7		df-ne	|- ( B =/= A <-> -. B = A )
8		pm2.24	|- ( B = A -> ( -. B = A -> A < B ) )
9	8	eqcoms	|- ( A = B -> ( -. B = A -> A < B ) )
10	7 9	syl5bi	|- ( A = B -> ( B =/= A -> A < B ) )
11	10	jao1i	|- ( ( A < B \/ A = B ) -> ( B =/= A -> A < B ) )
12	6 11	syl6bi	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( B =/= A -> A < B ) ) )
13	12	impd	|- ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B =/= A ) -> A < B ) )
14	5 13	impbid	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )