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