Metamath Proof Explorer


Theorem xrleltne

Description: 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 xrlttri3
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
2 simpl
 |-  ( ( -. A < B /\ -. B < A ) -> -. A < B )
3 1 2 syl6bi
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B -> -. A < B ) )
4 3 adantr
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A = B -> -. A < B ) )
5 xrleloe
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
6 5 biimpa
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A < B \/ A = B ) )
7 6 ord
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( -. A < B -> A = B ) )
8 4 7 impbid
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A = B <-> -. A < B ) )
9 8 necon2abid
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A < B <-> A =/= B ) )
10 necom
 |-  ( B =/= A <-> A =/= B )
11 9 10 bitr4di
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( A < B <-> B =/= A ) )
12 11 3impa
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A < B <-> B =/= A ) )