Theorem xeqlelt

Description: Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		xrletri3	|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
2		xrlenlt	|- ( ( B e. RR* /\ A e. RR* ) -> ( B <_ A <-> -. A < B ) )
3	2	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( B <_ A <-> -. A < B ) )
4	3	anbi2d	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A <_ B /\ B <_ A ) <-> ( A <_ B /\ -. A < B ) ) )
5	1 4	bitrd	|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )