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

Theorem eluzle 11173
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
eluzle  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )

Proof of Theorem eluzle
StepHypRef Expression
1 eluz2 11167 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp3bi 1023 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1869   class class class wbr 4421   ` cfv 5599    <_ cle 9678   ZZcz 10939   ZZ>=cuz 11161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-cnex 9597  ax-resscn 9598
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-fv 5607  df-ov 6306  df-neg 9865  df-z 10940  df-uz 11162
This theorem is referenced by:  uztrn  11177  uzneg  11179  uzss  11181  uz11  11183  eluzp1l  11185  uzm1  11191  uzin  11193  uzind4  11219  uzwo  11224  uzinfmiOLD  11241  uzsupss  11258  zgt1rpn0n1  11342  elfz5  11794  elfzle1  11804  elfzle2  11805  elfzle3  11807  uzsplit  11868  uzdisj  11869  uznfz  11879  elfz2nn0  11887  uzsubfz0  11900  nn0disj  11909  fzouzdisj  11956  expmulnbnd  12405  seqcoll  12626  swrdlen2  12797  swrdfv2  12798  rexuzre  13409  rlimclim1  13602  isercoll  13724  iseralt  13744  o1fsum  13866  mertenslem1  13933  fprodeq0  14022  efcllem  14125  rpnnen2lem9  14268  smuval2  14449  smupvallem  14450  hashdvds  14716  pcmpt2  14831  pcfaclem  14836  pcfac  14837  vdwlem6  14929  ramtlecl  14944  prmlem1  15072  prmlem2  15084  znfld  19123  lmnn  22225  mbflimsup  22615  mbflimsupOLD  22616  mbfi1fseqlem6  22670  dvfsumge  22966  plyco0  23138  coeeulem  23170  radcnvlem2  23361  log2tlbnd  23863  lgamgulmlem4  23949  lgamcvg2  23972  chtub  24132  chpval2  24138  chpchtsum  24139  bcmax  24198  bpos1lem  24202  bpos1  24203  bposlem3  24206  bposlem4  24207  bposlem5  24208  bposlem6  24209  lgslem1  24216  lgsdirprm  24249  lgseisen  24273  m1lgs  24282  dchrisumlema  24318  dchrisumlem2  24320  dchrisum0lem1  24346  axlowdimlem3  24966  axlowdimlem6  24969  axlowdimlem7  24970  axlowdimlem16  24979  axlowdimlem17  24980  constr3trllem3  25372  minvecolem3  26510  minvecolem4  26514  minvecolem3OLD  26520  minvecolem4OLD  26524  subfacval3  29914  climuzcnv  30317  poimirlem29  31927  fdc  32032  jm2.24nn  35773  jm2.23  35815  expdiophlem1  35840  isprm7  36562  hashnzfz2  36572  bccbc  36596  binomcxplemnn0  36600  fzdifsuc2  37416  uzfissfz  37435  iuneqfzuzlem  37443  ssuzfz  37458  fmul01lt1lem1  37526  climsuselem1  37550  climsuse  37551  ioodvbdlimc1lem2  37668  ioodvbdlimc1lem2OLD  37670  ioodvbdlimc2lem  37672  ioodvbdlimc2lemOLD  37673  iblspltprt  37714  itgspltprt  37720  stoweidlem11  37735  stirlinglem11  37810  fourierdlem79  37913  fourierdlem103  37937  fourierdlem104  37938  gboage9  38621  bgoldbnnsum3prm  38655  nnolog2flm1  39745
  Copyright terms: Public domain W3C validator