Metamath Proof Explorer


Theorem leltne

Description: 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999)

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

Proof

Step Hyp Ref Expression
1 lttri3
 |-  ( ( 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 leloe
 |-  ( ( 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 ) )