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

Theorem xrltnle 9652
Description: 'Less than' expressed in terms of 'less than or equal to', for extended reals. (Contributed by NM, 6-Feb-2007.)
Assertion
Ref Expression
xrltnle  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  <->  -.  B  <_  A ) )

Proof of Theorem xrltnle
StepHypRef Expression
1 xrlenlt 9651 . . 3  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( B  <_  A  <->  -.  A  <  B ) )
21con2bid 329 . 2  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( A  <  B  <->  -.  B  <_  A ) )
32ancoms 453 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 1767   class class class wbr 4447   RR*cxr 9626    < clt 9627    <_ cle 9628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-le 9633
This theorem is referenced by:  xrletri  11356  qextltlem  11400  xralrple  11403  xltadd1  11447  xsubge0  11452  xposdif  11453  xltmul1  11483  ioo0  11553  ico0  11574  ioc0  11575  snunioo  11645  snunioc  11647  difreicc  11651  hashbnd  12378  limsuplt  13264  pcadd  14266  pcadd2  14267  ramubcl  14394  ramlb  14395  leordtvallem1  19493  leordtvallem2  19494  leordtval2  19495  leordtval  19496  lecldbas  19502  blcld  20759  stdbdbl  20771  tmsxpsval2  20793  iocmnfcld  21027  xrsxmet  21065  metdsge  21104  bndth  21209  ovolgelb  21642  ovolunnul  21662  ioombl  21726  volsup2  21765  mbfmax  21807  ismbf3d  21812  itg2seq  21900  itg2monolem2  21909  itg2monolem3  21910  lhop2  22167  mdegleb  22215  deg1ge  22250  deg1add  22255  ig1pdvds  22328  plypf1  22360  radcnvlt1  22563  umgrafi  24014  xrdifh  27275  xrge00  27352  xrge0neqmnf  27357  gsumesum  27723  itg2gt0cn  29663  asindmre  29695  dvasin  29696  gtnelioc  31103  ltnelicc  31110  gtnelicc  31113  snunioo1  31132  lptioo2  31189  stoweidlem34  31350  fourierdlem20  31443  fouriersw  31548
  Copyright terms: Public domain W3C validator