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

Theorem xrltnle 9136
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 9135 . . 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 1725   class class class wbr 4204   RR*cxr 9111    < clt 9112    <_ cle 9113
This theorem is referenced by:  xrletri  10736  qextltlem  10780  xralrple  10783  xltadd1  10827  xsubge0  10832  xposdif  10833  xltmul1  10863  ioo0  10933  ico0  10954  ioc0  10955  snunioo  11015  difreicc  11020  hashbnd  11616  limsuplt  12265  pcadd  13250  pcadd2  13251  ramubcl  13378  ramlb  13379  leordtvallem1  17266  leordtvallem2  17267  leordtval2  17268  leordtval  17269  lecldbas  17275  blcld  18527  stdbdbl  18539  tmsxpsval2  18561  iocmnfcld  18795  xrsxmet  18832  metdsge  18871  bndth  18975  ovolgelb  19368  ovolunnul  19388  ioombl  19451  volsup2  19489  mbfmax  19533  ismbf3d  19538  itg2seq  19626  itg2monolem2  19635  itg2monolem3  19636  lhop2  19891  mdegleb  19979  deg1ge  20013  deg1add  20018  ig1pdvds  20091  plypf1  20123  radcnvlt1  20326  umgrafi  21349  snunioc  24129  xrdifh  24135  xrge00  24200  xrge0neqmnf  24204  gsumesum  24443  itg2gt0cn  26250  stoweidlem34  27750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4876  df-cnv 4878  df-le 9118
  Copyright terms: Public domain W3C validator