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

Theorem xrltnle 9656
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 9655 . . 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 1804   class class class wbr 4437   RR*cxr 9630    < clt 9631    <_ cle 9632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-le 9637
This theorem is referenced by:  xrletri  11366  qextltlem  11410  xralrple  11413  xltadd1  11457  xsubge0  11462  xposdif  11463  xltmul1  11493  ioo0  11563  ico0  11584  ioc0  11585  snunioo  11655  snunioc  11657  difreicc  11661  hashbnd  12390  limsuplt  13281  pcadd  14285  pcadd2  14286  ramubcl  14413  ramlb  14414  leordtvallem1  19584  leordtvallem2  19585  leordtval2  19586  leordtval  19587  lecldbas  19593  blcld  20881  stdbdbl  20893  tmsxpsval2  20915  iocmnfcld  21149  xrsxmet  21187  metdsge  21226  bndth  21331  ovolgelb  21764  ovolunnul  21784  ioombl  21848  volsup2  21887  mbfmax  21929  ismbf3d  21934  itg2seq  22022  itg2monolem2  22031  itg2monolem3  22032  lhop2  22289  mdegleb  22337  deg1ge  22372  deg1add  22377  ig1pdvds  22450  plypf1  22482  radcnvlt1  22685  umgrafi  24194  xrdifh  27463  xrge00  27547  xrge0neqmnf  27552  gsumesum  27940  itg2gt0cn  30045  asindmre  30077  dvasin  30078  radcnvrat  31171  gtnelioc  31459  ltnelicc  31466  gtnelicc  31469  snunioo1  31488  lptioo2  31545  stoweidlem34  31705  fourierdlem20  31798  fouriersw  31903
  Copyright terms: Public domain W3C validator