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

Theorem lenlt 9458
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 9434 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9434 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 9447 . 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 1756   class class class wbr 4297   RRcr 9286   RR*cxr 9422    < clt 9423    <_ cle 9424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-xp 4851  df-cnv 4853  df-xr 9427  df-le 9429
This theorem is referenced by:  ltnle  9459  letri3  9465  leloe  9466  eqlelt  9467  ne0gt0  9484  lelttric  9486  lenlti  9499  lenltd  9525  ltaddsub  9818  leord1  9872  lediv1  10199  suprleub  10299  dfinfmr  10312  infmrgelb  10315  nnge1  10353  nnnlt1  10357  avgle1  10569  avgle2  10570  nn0nlt0  10611  recnz  10722  btwnnz  10723  prime  10727  indstr  10928  uzsupss  10952  zbtwnre  10956  rpneg  11025  fzn  11471  fzonlt0  11577  fllt  11661  modifeq2int  11766  om2uzlt2i  11779  leexp2  11923  discr  12006  bcval4  12088  wrdsymb0  12264  ccatsymb  12286  swrdnd  12331  swrdvalodm2  12338  sqrneglem  12761  harmonic  13326  efle  13407  dvdsle  13583  infpnlem1  13976  pgpssslw  16118  dvferm1  21462  dvferm2  21464  dgrlt  21738  logleb  22057  argrege0  22065  ellogdm  22089  dvlog2lem  22102  cxple  22145  cxple3  22151  asinneg  22286  birthdaylem3  22352  ppieq0  22519  chpeq0  22552  chteq0  22553  lgsval2lem  22650  lgsneg  22663  lgsdilem  22666  ostth2lem1  22872  ostth3  22892  nmounbi  24181  nmlno0lem  24198  nmlnop0iALT  25404  supfz  27391  inffz  27392  fz0n  27394  leceifl  28425  lxflflp1  28426  ftc1anclem1  28472  nn0prpw  28523  nninfnub  28652  ellz1  29110  rencldnfilem  29164  subsubelfzo0  30215  clwlkisclwwlklem2a  30452  rusgranumwlks  30579  frgrareg  30715  friendship  30720  suppssfz  30791  fsuppmapnn0fiub0  30806  gsummoncoe1  30848  mp2pm2mplem4  30924
  Copyright terms: Public domain W3C validator