Theorem xrltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015)

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

Proof

Step	Hyp	Ref	Expression
1		xrlttri	|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
2		ioran	|- ( -. ( A = B \/ B < A ) <-> ( -. A = B /\ -. B < A ) )
3	2	biancomi	|- ( -. ( A = B \/ B < A ) <-> ( -. B < A /\ -. A = B ) )
4	1 3	bitrdi	|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> ( -. B < A /\ -. A = B ) ) )
5		xrlenlt	|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
6		nesym	|- ( B =/= A <-> -. A = B )
7	6	a1i	|- ( ( A e. RR* /\ B e. RR* ) -> ( B =/= A <-> -. A = B ) )
8	5 7	anbi12d	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A <_ B /\ B =/= A ) <-> ( -. B < A /\ -. A = B ) ) )
9	4 8	bitr4d	|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )