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

Theorem xrlenlt 9688
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 4418 . . 3  |-  ( A  <_  B  <->  <. A ,  B >.  e.  <_  )
2 opelxpi 4877 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  <. A ,  B >.  e.  ( RR*  X. 
RR* ) )
3 df-le 9670 . . . . . . 7  |-  <_  =  ( ( RR*  X.  RR* )  \  `'  <  )
43eleq2i 2498 . . . . . 6  |-  ( <. A ,  B >.  e. 
<_ 
<-> 
<. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )
)
5 eldif 3443 . . . . . 6  |-  ( <. A ,  B >.  e.  ( ( RR*  X.  RR* )  \  `'  <  )  <->  (
<. A ,  B >.  e.  ( RR*  X.  RR* )  /\  -.  <. A ,  B >.  e.  `'  <  )
)
64, 5bitri 252 . . . . 5  |-  ( <. A ,  B >.  e. 
<_ 
<->  ( <. A ,  B >.  e.  ( RR*  X.  RR* )  /\  -.  <. A ,  B >.  e.  `'  <  ) )
76baib 911 . . . 4  |-  ( <. A ,  B >.  e.  ( RR*  X.  RR* )  ->  ( <. A ,  B >.  e.  <_  <->  -.  <. A ,  B >.  e.  `'  <  ) )
82, 7syl 17 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e. 
<_ 
<->  -.  <. A ,  B >.  e.  `'  <  )
)
91, 8syl5bb 260 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  <. A ,  B >.  e.  `'  <  ) )
10 opelcnvg 5025 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( <. A ,  B >.  e.  `'  <  <->  <. B ,  A >.  e.  <  ) )
11 df-br 4418 . . . 4  |-  ( B  <  A  <->  <. B ,  A >.  e.  <  )
1210, 11syl6rbbr 267 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( B  <  A  <->  <. A ,  B >.  e.  `'  <  ) )
1312notbid 295 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( -.  B  <  A  <->  -.  <. A ,  B >.  e.  `'  <  ) )
149, 13bitr4d 259 1  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    e. wcel 1867    \ cdif 3430   <.cop 3999   class class class wbr 4417    X. cxp 4843   `'ccnv 4844   RR*cxr 9663    < clt 9664    <_ cle 9665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-xp 4851  df-cnv 4853  df-le 9670
This theorem is referenced by:  xrlenltd  9689  xrltnle  9690  xrnltled  9691  lenlt  9701  pnfge  11421  mnfle  11424  xrleloe  11432  xrltlen  11434  xrletri3  11440  xralrple  11487  xleneg  11500  supxr2  11588  supxrbnd1  11596  supxrbnd2  11597  supxrub  11599  supxrleub  11601  supxrbnd  11603  infxrgelb  11610  infmxrlbOLD  11613  infmxrgelbOLD  11614  ixxub  11645  ixxlbOLD  11647  ioon0  11651  iccid  11670  icc0  11673  icoun  11743  icodisj  11744  snunico  11746  ioodisj  11749  ioojoin  11750  supicclub2  11770  hashgt0elex  12564  hashgt12el  12579  hashgt12el2  12580  0ringnnzr  18434  lecldbas  20172  xmetgt0  21310  bldisj  21350  icopnfcld  21725  icombl  22424  ioombl  22425  ioorcl2  22431  vitalilem4  22476  itg2gt0  22625  ply1divmo  22993  ig1peu  23029  ig1peuOLD  23030  radcnvle  23279  psercnlem1  23284  nmlnogt0  26324  xgepnf  28211  xlemnf  28212  xrlelttric  28213  xrsupssd  28221  xrge0infss  28222  xrge0infssd  28223  infxrge0gelb  28228  joiniooico  28233  xeqlelt  28235  iocinif  28240  esumsnf  28765  esum2d  28794  oms0  28999  omssubadd  29002  relowlpssretop  31542  mblfinlem3  31727  mblfinlem4  31728  ismblfin  31729  asindmre  31775  ioounsn  35841  iocmbl  35844  supxrgere  37213  snunioo2  37239  iccdifprioo  37250  iccpartnel  38199
  Copyright terms: Public domain W3C validator