Metamath Proof Explorer


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 ) ) )