MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrlenlt Structured version   Unicode version

Theorem xrlenlt 9641
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
StepHypRef Expression
1 df-br 4441 . . 3  |-  ( A  <_  B  <->  <. A ,  B >.  e.  <_  )
2 opelxpi 5023 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  <. A ,  B >.  e.  ( RR*  X. 
RR* ) )
3 df-le 9623 . . . . . . 7  |-  <_  =  ( ( RR*  X.  RR* )  \  `'  <  )
43eleq2i 2538 . . . . . 6  |-  ( <. A ,  B >.  e. 
<_ 
<-> 
<. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )
)
5 eldif 3479 . . . . . 6  |-  ( <. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )  <->  (
<. A ,  B >.  e.  ( RR*  X.  RR* )  /\  -.  <. A ,  B >.  e.  `'  <  )
)
64, 5bitri 249 . . . . 5  |-  ( <. A ,  B >.  e. 
<_ 
<->  ( <. A ,  B >.  e.  ( RR*  X.  RR* )  /\  -.  <. A ,  B >.  e.  `'  <  ) )
76baib 898 . . . 4  |-  ( <. A ,  B >.  e.  ( RR*  X.  RR* )  ->  ( <. A ,  B >.  e.  <_  <->  -.  <. A ,  B >.  e.  `'  <  ) )
82, 7syl 16 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e. 
<_ 
<->  -.  <. A ,  B >.  e.  `'  <  )
)
91, 8syl5bb 257 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  <. A ,  B >.  e.  `'  <  ) )
10 opelcnvg 5173 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e.  `'  <  <->  <. B ,  A >.  e.  <  ) )
11 df-br 4441 . . . 4  |-  ( B  <  A  <->  <. B ,  A >.  e.  <  )
1210, 11syl6rbbr 264 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( B  <  A  <->  <. A ,  B >.  e.  `'  <  ) )
1312notbid 294 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( -.  B  <  A  <->  -.  <. A ,  B >.  e.  `'  <  ) )
149, 13bitr4d 256 1  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1762    \ cdif 3466   <.cop 4026   class class class wbr 4440    X. cxp 4990   `'ccnv 4991   RR*cxr 9616    < clt 9617    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-xp 4998  df-cnv 5000  df-le 9623
This theorem is referenced by:  xrltnle  9642  lenlt  9652  pnfge  11328  mnfle  11331  xrleloe  11339  xrltlen  11341  xrletri3  11347  xralrple  11393  xleneg  11406  supxr2  11494  supxrbnd1  11502  supxrbnd2  11503  supxrub  11505  supxrleub  11507  supxrbnd  11509  infmxrlb  11514  infmxrgelb  11515  ixxub  11539  ixxlb  11540  ioon0  11544  iccid  11563  icc0  11566  icoun  11633  icodisj  11634  snunico  11636  ioodisj  11639  ioojoin  11640  supicclub2  11660  hashgt0elex  12419  hashgt12el  12433  hashgt12el2  12434  lecldbas  19479  xmetgt0  20589  bldisj  20629  icopnfcld  21003  icombl  21702  ioombl  21703  ioorcl2  21709  vitalilem4  21748  itg2gt0  21895  ply1divmo  22264  ig1peu  22300  radcnvle  22542  psercnlem1  22547  nmlnogt0  25238  xgepnf  27088  xlemnf  27089  xrlelttric  27090  xrsupssd  27097  xrge0infss  27098  xrge0infssd  27099  joiniooico  27103  xeqlelt  27105  iocinif  27110  esumsn  27562  oms0  27756  mblfinlem3  29481  mblfinlem4  29482  ismblfin  29483  asindmre  29530  ioounsn  30635  iocmbl  30638  xrnltled  30884  snunioo2  30927  iccdifprioo  30939  0rngnnzr  31906
  Copyright terms: Public domain W3C validator