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

Theorem xrltnle 9078
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 9077 . . 3  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( B  <_  A  <->  -.  A  <  B ) )
21con2bid 320 . 2  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( A  <  B  <->  -.  B  <_  A ) )
32ancoms 440 1  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  <->  -.  B  <_  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1717   class class class wbr 4154   RR*cxr 9053    < clt 9054    <_ cle 9055
This theorem is referenced by:  xrletri  10677  qextltlem  10721  xralrple  10724  xltadd1  10768  xsubge0  10773  xposdif  10774  xltmul1  10804  ioo0  10874  ico0  10895  ioc0  10896  snunioo  10956  difreicc  10961  hashbnd  11552  limsuplt  12201  pcadd  13186  pcadd2  13187  ramubcl  13314  ramlb  13315  leordtvallem1  17197  leordtvallem2  17198  leordtval2  17199  leordtval  17200  lecldbas  17206  blcld  18426  stdbdbl  18438  tmsxpsval2  18460  iocmnfcld  18675  xrsxmet  18712  metdsge  18751  bndth  18855  ovolgelb  19244  ovolunnul  19264  ioombl  19327  volsup2  19365  mbfmax  19409  ismbf3d  19414  itg2seq  19502  itg2monolem2  19511  itg2monolem3  19512  lhop2  19767  mdegleb  19855  deg1ge  19889  deg1add  19894  ig1pdvds  19967  plypf1  19999  radcnvlt1  20202  umgrafi  21225  snunioc  23974  xrdifh  23980  xrge00  24038  xrge0neqmnf  24042  gsumesum  24248  itg2gt0cn  25961  stoweidlem34  27452
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-br 4155  df-opab 4209  df-xp 4825  df-cnv 4827  df-le 9060
  Copyright terms: Public domain W3C validator