Metamath Proof Explorer

Theorem xrlenlt

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( A <_ B <-> <. A , B >. e. <_ )
2 opelxpi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> <. A , B >. e. ( RR* X. RR* ) )
3 df-le 
 |-  <_ = ( ( RR* X. RR* ) \ `' < )
4 3 eleq2i 
 |-  ( <. A , B >. e. <_ <-> <. A , B >. e. ( ( RR* X. RR* ) \ `' < ) )
5 eldif 
 |-  ( <. A , B >. e. ( ( RR* X. RR* ) \ `' < ) <-> ( <. A , B >. e. ( RR* X. RR* ) /\ -. <. A , B >. e. `' < ) )
6 4 5 bitri 
 |-  ( <. A , B >. e. <_ <-> ( <. A , B >. e. ( RR* X. RR* ) /\ -. <. A , B >. e. `' < ) )
7 6 baib 
 |-  ( <. A , B >. e. ( RR* X. RR* ) -> ( <. A , B >. e. <_ <-> -. <. A , B >. e. `' < ) )
8 2 7 syl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( <. A , B >. e. <_ <-> -. <. A , B >. e. `' < ) )
9 1 8 syl5bb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. <. A , B >. e. `' < ) )
10 df-br 
 |-  ( B < A <-> <. B , A >. e. < )
11 opelcnvg 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( <. A , B >. e. `' < <-> <. B , A >. e. < ) )
12 10 11 bitr4id 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B < A <-> <. A , B >. e. `' < ) )
13 12 notbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. B < A <-> -. <. A , B >. e. `' < ) )
14 9 13 bitr4d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )