This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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