Theorem eluzle 12852

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzle	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Proof of Theorem eluzle

Step	Hyp	Ref	Expression
1		eluz2 12845	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp3bi 1160	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  ‘cfv 6521   ≤ cle 11217  ℤcz 12568  ℤ_≥cuz 12839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569  df-uz 12840

This theorem is referenced by:  uztrn  12857  uzneg  12859  uzss  12862  uz11  12864  eluzp1l  12866  eluzadd  12868  eluzsub  12869  subeluzsub  12872  uzm1  12873  uzin  12875  uzind4  12907  uzwo  12912  uzsupss  12941  ge2halflem1  13110  elfz5  13521  elfzle1  13532  elfzle2  13533  elfzle3  13535  elfz1uz  13599  uzsplit  13601  uzdisj  13602  uznfz  13615  elfz2nn0  13623  uzsubfz0  13641  nn0disj  13649  fzouzdisj  13701  fzoun  13702  fldiv4lem1div2uz2  13846  m1modge3gt1  13931  expmulnbnd  14248  seqcoll  14477  swrdlen2  14674  swrdfv2  14675  rexuzre  15380  rlimclim1  15572  isercoll  15695  iseralt  15712  o1fsum  15841  mertenslem1  15914  fprodeq0  16005  efcllem  16107  rpnnen2lem9  16254  smuval2  16516  smupvallem  16517  isprm7  16743  hashdvds  16810  pcmpt2  16929  pcfaclem  16934  pcfac  16935  vdwlem6  17022  ramtlecl  17036  prmlem1  17143  prmlem2  17156  znfld  21612  lmnn  25325  mbflimsup  25728  mbfi1fseqlem6  25782  dvfsumge  26084  plyco0  26252  coeeulem  26284  radcnvlem2  26477  log2tlbnd  27010  lgamgulmlem4  27096  lgamcvg2  27119  chtub  27276  chpval2  27282  chpchtsum  27283  bcmax  27342  bpos1lem  27346  bpos1  27347  bposlem3  27350  bposlem4  27351  bposlem5  27352  bposlem6  27353  lgslem1  27361  lgsdirprm  27395  lgseisen  27443  dchrisumlema  27552  dchrisumlem2  27554  dchrisum0lem1  27580  axlowdimlem3  29145  axlowdimlem6  29148  axlowdimlem7  29149  axlowdimlem16  29158  axlowdimlem17  29159  dlwwlknondlwlknonf1olem1  30566  minvecolem3  31079  minvecolem4  31083  breprexplemc  34926  subfacval3  35539  climuzcnv  36021  knoppndvlem6  36955  poimirlem29  38148  fdc  38244  aks4d1lem1  42679  aks4d1p1  42693  aks4d1p2  42694  aks4d1p3  42695  aks4d1p5  42697  aks4d1p6  42698  aks4d1p7d1  42699  aks4d1p7  42700  aks4d1p8  42704  aks4d1p9  42705  aks6d1c7lem1  42797  aks6d1c7lem2  42798  aks6d1c7  42801  aks5lem6  42809  aks5lem8  42818  jm2.24nn  43536  jm2.23  43573  expdiophlem1  43598  hashnzfz2  44897  bccbc  44921  binomcxplemnn0  44925  ssinc  45665  ssdec  45666  fzdifsuc2  45889  uzfissfz  45902  iuneqfzuzlem  45910  ssuzfz  45925  uzublem  46004  uzinico  46135  fmul01lt1lem1  46160  climsuselem1  46183  climsuse  46184  limsupubuzlem  46286  limsupequzlem  46296  limsupmnfuzlem  46300  limsupre3uzlem  46309  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  iblspltprt  46547  itgspltprt  46553  stoweidlem11  46585  stirlinglem11  46658  fourierdlem79  46759  fourierdlem103  46783  fourierdlem104  46784  vonioolem1  47254  nnmul2  47924  2ltceilhalf  47926  ceilhalfnn  47934  2timesltsq  47972  2timesltsqm1  47973  fmtnoprmfac1  48174  fmtnoprmfac2lem1  48175  lighneallem2  48215  lighneallem4a  48217  gboge9  48386  bgoldbnnsum3prm  48426  nnolog2flm1  49212