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

Theorem eluzle 11083
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 11077 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp3bi 1008 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   class class class wbr 4440   ` cfv 5579    <_ cle 9618   ZZcz 10853   ZZ>=cuz 11071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587  df-ov 6278  df-neg 9797  df-z 10854  df-uz 11072
This theorem is referenced by:  uztrn  11087  uzneg  11089  uzss  11091  uz11  11093  eluzp1l  11095  uzm1  11101  uzin  11103  uzind4  11128  uzwo  11133  uzwoOLD  11134  uzinfmi  11150  uzsupss  11163  elfz5  11669  elfzle1  11678  elfzle2  11679  elfzle3  11681  uzsplit  11739  uzdisj  11740  uznfz  11750  elfz2nn0  11757  uzsubfz0  11769  nn0disj  11777  fzouzdisj  11818  expmulnbnd  12253  seqcoll  12465  rexuzre  13134  rlimclim1  13317  isercoll  13439  iseralt  13456  o1fsum  13576  mertenslem1  13645  efcllem  13664  rpnnen2lem9  13806  smuval2  13980  smupvallem  13981  hashdvds  14153  pcmpt2  14260  pcfaclem  14265  pcfac  14266  vdwlem6  14352  ramtlecl  14366  prmlem1  14440  prmlem2  14452  znfld  18359  lmnn  21430  mbflimsup  21801  mbfi1fseqlem6  21855  dvfsumge  22151  plyco0  22317  coeeulem  22349  radcnvlem2  22536  log2tlbnd  22997  chtub  23208  chpval2  23214  chpchtsum  23215  bcmax  23274  bpos1lem  23278  bpos1  23279  bposlem3  23282  bposlem4  23283  bposlem5  23284  bposlem6  23285  lgslem1  23292  lgsdirprm  23325  lgseisen  23349  m1lgs  23358  dchrisumlema  23394  dchrisumlem2  23396  dchrisum0lem1  23422  axlowdimlem3  23916  axlowdimlem6  23919  axlowdimlem7  23920  axlowdimlem16  23929  axlowdimlem17  23930  constr3trllem3  24314  minvecolem3  25454  minvecolem4  25458  rnlogblem  27641  lgamgulmlem4  28200  lgamcvg2  28223  subfacval3  28259  climuzcnv  28498  fprodeq0  28668  fdc  29828  jm2.24nn  30488  jm2.23  30531  expdiophlem1  30556  fmul01lt1lem1  31089  climsuselem1  31104  climsuse  31105  ioodvbdlimc1lem2  31217  ioodvbdlimc2lem  31219  iblspltprt  31246  itgspltprt  31252  stoweidlem11  31266  stirlinglem11  31339  fourierdlem79  31441  fourierdlem103  31465  fourierdlem104  31466
  Copyright terms: Public domain W3C validator