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

Theorem eluzle 10876
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 10870 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp3bi 1005 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   class class class wbr 4295   ` cfv 5421    <_ cle 9422   ZZcz 10649   ZZ>=cuz 10864
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-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-cnex 9341  ax-resscn 9342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  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 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-ov 6097  df-neg 9601  df-z 10650  df-uz 10865
This theorem is referenced by:  uztrn  10880  uzneg  10882  uzss  10884  uz11  10886  eluzp1l  10888  uzm1  10894  uzin  10896  uzind4  10915  uzwo  10920  uzwoOLD  10921  uzinfmi  10937  uzsupss  10950  elfz5  11448  elfzle1  11457  elfzle2  11458  elfzle3  11460  elfz2nn0  11483  uzsplit  11533  uzdisj  11534  uznfz  11546  fzouzdisj  11588  expmulnbnd  11999  seqcoll  12219  rexuzre  12843  rlimclim1  13026  isercoll  13148  iseralt  13165  o1fsum  13279  mertenslem1  13347  efcllem  13366  rpnnen2lem9  13508  smuval2  13681  smupvallem  13682  hashdvds  13853  pcmpt2  13958  pcfaclem  13963  pcfac  13964  vdwlem6  14050  ramtlecl  14064  prmlem1  14138  prmlem2  14150  znfld  17996  lmnn  20777  mbflimsup  21147  mbfi1fseqlem6  21201  dvfsumge  21497  plyco0  21663  coeeulem  21695  radcnvlem2  21882  log2tlbnd  22343  chtub  22554  chpval2  22560  chpchtsum  22561  bcmax  22620  bpos1lem  22624  bpos1  22625  bposlem3  22628  bposlem4  22629  bposlem5  22630  bposlem6  22631  lgslem1  22638  lgsdirprm  22671  lgseisen  22695  m1lgs  22704  dchrisumlema  22740  dchrisumlem2  22742  dchrisum0lem1  22768  axlowdimlem3  23193  axlowdimlem6  23196  axlowdimlem7  23197  axlowdimlem16  23206  axlowdimlem17  23207  constr3trllem3  23541  minvecolem3  24280  minvecolem4  24284  rnlogblem  26461  lgamgulmlem4  27021  lgamcvg2  27044  subfacval3  27080  climuzcnv  27319  fprodeq0  27489  fdc  28644  jm2.24nn  29305  jm2.23  29348  expdiophlem1  29373  fmul01lt1lem1  29768  climsuselem1  29783  climsuse  29784  stoweidlem11  29809  stirlinglem11  29882  uzsubfz0  30208
  Copyright terms: Public domain W3C validator