Theorem xrlenlt 8139

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

Assertion

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

Proof of Theorem xrlenlt

Step	Hyp	Ref	Expression
1		df-br 4046	. . 3 |- ( A <_ B <-> <. A , B >. e. <_ )
2		opelxpi 4708	. . . 4 |- ( ( A e. RR* /\ B e. RR* ) -> <. A , B >. e. ( RR* X. RR* ) )
3		df-le 8115	. . . . . . 7 |- <_ = ( ( RR* X. RR* ) \ `' < )
4	3	eleq2i 2272	. . . . . 6 |- ( <. A , B >. e. <_ <-> <. A , B >. e. ( ( RR* X. RR* ) \ `' < ) )
5		eldif 3175	. . . . . 6 |- ( <. A , B >. e. ( ( RR* X. RR* ) \ `' < ) <-> ( <. A , B >. e. ( RR* X. RR* ) /\ -. <. A , B >. e. `' < ) )
6	4, 5	bitri 184	. . . . 5 |- ( <. A , B >. e. <_ <-> ( <. A , B >. e. ( RR* X. RR* ) /\ -. <. A , B >. e. `' < ) )
7	6	baib 921	. . . 4 |- ( <. A , B >. e. ( RR* X. RR* ) -> ( <. A , B >. e. <_ <-> -. <. A , B >. e. `' < ) )
8	2, 7	syl 14	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( <. A , B >. e. <_ <-> -. <. A , B >. e. `' < ) )
9	1, 8	bitrid 192	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. <. A , B >. e. `' < ) )
10		df-br 4046	. . . 4 |- ( B < A <-> <. B , A >. e. < )
11		opelcnvg 4859	. . . 4 |- ( ( A e. RR* /\ B e. RR* ) -> ( <. A , B >. e. `' < <-> <. B , A >. e. < ) )
12	10, 11	bitr4id 199	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( B < A <-> <. A , B >. e. `' < ) )
13	12	notbid 669	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( -. B < A <-> -. <. A , B >. e. `' < ) )
14	9, 13	bitr4d 191	1 |- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2176   \ cdif 3163   <.cop 3636   class class class wbr 4045   X. cxp 4674   `'ccnv 4675   RR*cxr 8108   < clt 8109   <_ cle 8110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046  df-opab 4107  df-xp 4682  df-cnv 4684  df-le 8115

This theorem is referenced by:  lenlt  8150  pnfge  9913  mnfle  9916  xrltle  9922  xrleid  9924  xnn0dcle  9926  xrletri3  9928  xrlelttr  9930  xrltletr  9931  xrletr  9932  xgepnf  9940  xleneg  9961  xltadd1  10000  xsubge0  10005  xleaddadd  10011  iccid  10049  icc0r  10050  icodisj  10116  ioodisj  10117  ioo0  10404  ico0  10406  ioc0  10407  leisorel  10984  xrmaxleim  11588  xrmaxiflemval  11594  xrmaxlesup  11603  xrmaxaddlem  11604  xrminmax  11609  pcadd  12696  bldisj  14906  bdxmet  15006  bdbl  15008