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

Theorem xrltnle 8893
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 8892 . . 3  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( B  <_  A  <->  -.  A  <  B ) )
21con2bid 319 . 2  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( A  <  B  <->  -.  B  <_  A ) )
32ancoms 439 1  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  <->  -.  B  <_  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1686   class class class wbr 4025   RR*cxr 8868    < clt 8869    <_ cle 8870
This theorem is referenced by:  xrletri  10487  qextltlem  10531  xralrple  10534  xltadd1  10578  xsubge0  10583  xposdif  10584  xltmul1  10614  ioo0  10683  ico0  10704  ioc0  10705  snunioo  10764  difreicc  10769  hashbnd  11345  limsuplt  11955  pcadd  12939  pcadd2  12940  ramubcl  13067  ramlb  13068  leordtvallem1  16942  leordtvallem2  16943  leordtval2  16944  leordtval  16945  lecldbas  16951  blcld  18053  stdbdbl  18065  tmsxpsval2  18087  iocmnfcld  18280  xrsxmet  18317  metdsge  18355  bndth  18458  ovolgelb  18841  ovolunnul  18861  ioombl  18924  volsup2  18962  mbfmax  19006  ismbf3d  19011  itg2seq  19099  itg2monolem2  19108  itg2monolem3  19109  lhop2  19364  mdegleb  19452  deg1ge  19486  deg1add  19491  ig1pdvds  19564  plypf1  19596  radcnvlt1  19796  snunioc  23269  xrdifh  23275  xrge00  23313  xrge0neqmnf  23332  umgrafi  23876  supnuf  25640  supexr  25642  stoweidlem34  27794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4697  df-cnv 4699  df-le 8875
  Copyright terms: Public domain W3C validator