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

Theorem lenlt 9663
Description: 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
Assertion
Ref Expression
lenlt  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )

Proof of Theorem lenlt
StepHypRef Expression
1 rexr 9639 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9639 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 9652 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2an 477 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   RRcr 9491   RR*cxr 9627    < clt 9628    <_ cle 9629
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-xr 9632  df-le 9634
This theorem is referenced by:  ltnle  9664  letri3  9670  leloe  9671  eqlelt  9672  ne0gt0  9689  lelttric  9691  lenlti  9704  lenltd  9730  ltaddsub  10026  leord1  10080  lediv1  10407  suprleub  10507  dfinfmr  10520  infmrgelb  10523  nnge1  10562  nnnlt1  10566  avgle1  10778  avgle2  10779  nn0nlt0  10822  recnz  10936  btwnnz  10937  prime  10941  indstr  11150  uzsupss  11174  zbtwnre  11180  rpneg  11249  fzn  11702  fzonlt0  11816  fllt  11911  flflp1  11912  modifeq2int  12017  om2uzlt2i  12030  fsuppmapnn0fiub0  12067  suppssfz  12068  leexp2  12188  discr  12271  bcval4  12353  wrdsymb0  12540  ccatsymb  12565  swrdnd  12620  swrdvalodm2  12627  sqrtneglem  13063  harmonic  13633  efle  13714  dvdsle  13890  infpnlem1  14287  pgpssslw  16440  gsummoncoe1  18145  mp2pm2mplem4  19105  dvferm1  22149  dvferm2  22151  dgrlt  22425  logleb  22744  argrege0  22752  ellogdm  22776  dvlog2lem  22789  cxple  22832  cxple3  22838  asinneg  22973  birthdaylem3  23039  ppieq0  23206  chpeq0  23239  chteq0  23240  lgsval2lem  23337  lgsneg  23350  lgsdilem  23353  ostth2lem1  23559  ostth3  23579  clwlkisclwwlklem2a  24489  rusgranumwlks  24660  frgrareg  24822  friendship  24827  nmounbi  25395  nmlno0lem  25412  nmlnop0iALT  26618  supfz  28610  inffz  28611  fz0n  28613  leceifl  29649  ftc1anclem1  29695  nn0prpw  29746  nninfnub  29875  ellz1  30332  rencldnfilem  30386  icccncfext  31254  cncfiooicclem1  31260  subsubelfzo0  31833
  Copyright terms: Public domain W3C validator