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

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 biimtrid 
 |-  ( A = B -> ( B =/= A -> A < B ) )
11 10 jao1i 
 |-  ( ( A < B \/ A = B ) -> ( B =/= A -> A < B ) )
12 6 11 biimtrdi 
 |-  ( ( 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 ) ) )