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

Theorem lenlt 9684
Description: 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
Assertion
Ref Expression
lenlt

Proof of Theorem lenlt
StepHypRef Expression
1 rexr 9660 . 2
2 rexr 9660 . 2
3 xrlenlt 9673 . 2
41, 2, 3syl2an 477 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818   class class class wbr 4452   cr 9512   cxr 9648   clt 9649   cle 9650
This theorem is referenced by:  ltnle  9685  letri3  9691  leloe  9692  eqlelt  9693  ne0gt0  9710  lelttric  9712  lenlti  9725  lenltd  9752  ltaddsub  10051  leord1  10105  lediv1  10432  suprleub  10532  dfinfmr  10545  infmrgelb  10548  nnge1  10587  nnnlt1  10591  avgle1  10803  avgle2  10804  nn0nlt0  10847  recnz  10963  btwnnz  10964  prime  10968  indstr  11179  uzsupss  11203  zbtwnre  11209  rpneg  11278  fzn  11731  fzonlt0  11848  fllt  11943  flflp1  11944  modifeq2int  12049  om2uzlt2i  12062  fsuppmapnn0fiub0  12099  suppssfz  12100  leexp2  12220  discr  12303  bcval4  12385  wrdsymb0  12575  ccatsymb  12600  swrdnd  12657  swrdvalodm2  12664  sqrtneglem  13100  harmonic  13670  efle  13853  dvdsle  14031  infpnlem1  14428  pgpssslw  16634  gsummoncoe1  18346  mp2pm2mplem4  19310  dvferm1  22386  dvferm2  22388  dgrlt  22663  logleb  22988  argrege0  22996  ellogdm  23020  dvlog2lem  23033  cxple  23076  cxple3  23082  asinneg  23217  birthdaylem3  23283  ppieq0  23450  chpeq0  23483  chteq0  23484  lgsval2lem  23581  lgsneg  23594  lgsdilem  23597  ostth2lem1  23803  ostth3  23823  clwlkisclwwlklem2a  24785  rusgranumwlks  24956  frgrareg  25117  friendship  25122  nmounbi  25691  nmlno0lem  25708  nmlnop0iALT  26914  supfz  29107  inffz  29108  fz0n  29110  leceifl  30044  ftc1anclem1  30090  nn0prpw  30141  nninfnub  30244  ellz1  30700  rencldnfilem  30754  icccncfext  31690  subsubelfzo0  32338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-cnv 5012  df-xr 9653  df-le 9655
  Copyright terms: Public domain W3C validator