Metamath Proof Explorer


Theorem ltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999)

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

Proof

Step Hyp Ref Expression
1 ltle
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
2 ltne
 |-  ( ( A e. RR /\ A < B ) -> B =/= A )
3 2 ex
 |-  ( A e. RR -> ( A < B -> B =/= A ) )
4 3 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> B =/= A ) )
5 1 4 jcad
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> ( A <_ B /\ B =/= A ) ) )
6 leloe
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
7 df-ne
 |-  ( B =/= A <-> -. B = A )
8 pm2.24
 |-  ( B = A -> ( -. B = A -> A < B ) )
9 8 eqcoms
 |-  ( A = B -> ( -. B = A -> A < B ) )
10 7 9 syl5bi
 |-  ( A = B -> ( B =/= A -> A < B ) )
11 10 jao1i
 |-  ( ( A < B \/ A = B ) -> ( B =/= A -> A < B ) )
12 6 11 syl6bi
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( B =/= A -> A < B ) ) )
13 12 impd
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B =/= A ) -> A < B ) )
14 5 13 impbid
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )