Theorem eluzelz 12765

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

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

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 12761	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1147	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5099  ‘cfv 6493   ≤ cle 11171  ℤcz 12492  ℤ_≥cuz 12755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-cnex 11086  ax-resscn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7363  df-neg 11371  df-z 12493  df-uz 12756

This theorem is referenced by:  eluzelre  12766  uztrn  12773  uzneg  12775  uzss  12778  eluzp1l  12782  eluzadd  12784  eluzsub  12785  subeluzsub  12788  uzm1  12789  uzin  12791  uzind4  12823  uzwo  12828  uz2mulcl  12843  uzsupss  12857  elfz5  13436  elfzel2  13442  elfzelz  13444  eluzfz2  13452  peano2fzr  13457  fzsplit2  13469  fzopth  13481  ssfzunsn  13490  fzsuc  13491  elfz1uz  13514  uzsplit  13516  uzdisj  13517  fzm1  13527  uznfz  13530  nn0disj  13564  preduz  13570  elfzo3  13596  fzoss2  13607  fzouzsplit  13614  fzoun  13616  eluzgtdifelfzo  13647  fzosplitsnm1  13660  fzofzp1b  13685  elfzonelfzo  13689  fzosplitsn  13696  fzisfzounsn  13700  fldiv4lem1div2uz2  13760  m1modge3gt1  13845  modaddmodup  13861  om2uzlti  13877  om2uzf1oi  13880  uzrdgxfr  13894  fzen2  13896  seqfveq2  13951  seqfeq2  13952  seqshft2  13955  monoord  13959  monoord2  13960  sermono  13961  seqsplit  13962  seqf1olem1  13968  seqf1olem2  13969  seqid  13974  leexp2a  14099  expnlbnd2  14161  expmulnbnd  14162  hashfz  14354  fzsdom2  14355  hashfzo  14356  hashfzp1  14358  seqcoll  14391  swrdfv2  14589  pfxccatin12  14660  rexuz3  15276  r19.2uz  15279  rexuzre  15280  cau4  15284  caubnd2  15285  clim  15421  climrlim2  15474  climshft2  15509  climaddc1  15562  climmulc2  15564  climsubc1  15565  climsubc2  15566  clim2ser  15582  clim2ser2  15583  iserex  15584  climlec2  15586  climub  15589  isercolllem2  15593  isercoll  15595  isercoll2  15596  climcau  15598  caurcvg2  15605  caucvgb  15607  serf0  15608  iseraltlem1  15609  iseraltlem2  15610  iseralt  15612  sumrblem  15638  fsumcvg  15639  summolem2a  15642  fsumcvg2  15654  fsumm1  15678  fzosump1  15679  fsump1  15683  fsumrev2  15709  telfsumo  15729  fsumparts  15733  isumsplit  15767  isumrpcl  15770  isumsup2  15773  cvgrat  15810  mertenslem1  15811  clim2div  15816  prodeq2ii  15838  fprodcvg  15857  prodmolem2a  15861  zprod  15864  fprodntriv  15869  fprodser  15876  fprodm1  15894  fprodp1  15896  fprodeq0  15902  isprm3  16614  nprm  16619  dvdsprm  16634  exprmfct  16635  isprm5  16638  maxprmfct  16640  prmdvdsncoprmbd  16658  ncoprmlnprm  16659  phibndlem  16701  dfphi2  16705  hashdvds  16706  pcaddlem  16820  pcfac  16831  expnprm  16834  prmreclem4  16851  vdwlem8  16920  gsumval2a  18614  efgs1b  19669  telgsumfzs  19922  iscau4  25239  caucfil  25243  iscmet3lem3  25250  iscmet3lem1  25251  iscmet3lem2  25252  lmle  25261  uniioombllem3  25546  mbflimsup  25627  mbfi1fseqlem6  25681  dvfsumle  25986  dvfsumleOLD  25987  dvfsumge  25988  dvfsumabs  25989  aaliou3lem1  26310  aaliou3lem2  26311  ulmres  26357  ulmshftlem  26358  ulmshft  26359  ulmcaulem  26363  ulmcau  26364  ulmdvlem1  26369  radcnvlem1  26382  logblt  26754  logbgcd1irr  26764  muval1  27103  chtdif  27128  ppidif  27133  chtub  27183  bcmono  27248  bpos1lem  27253  lgsquad2lem2  27356  2sqlem6  27394  2sqlem8a  27396  2sqlem8  27397  chebbnd1lem1  27440  dchrisumlem2  27461  dchrisum0lem1  27487  ostthlem2  27599  ostth2  27608  axlowdimlem3  29000  axlowdimlem6  29003  axlowdimlem7  29004  axlowdimlem16  29013  axlowdimlem17  29014  axlowdim  29017  clwwnrepclwwn  30402  fzspl  32850  fzdif2  32851  supfz  35904  divcnvlin  35908  nn0prpwlem  36497  fdc  37917  mettrifi  37929  caushft  37933  aks4d1lem1  42353  aks4d1p1  42367  aks4d1p2  42368  aks4d1p3  42369  aks4d1p5  42371  aks4d1p6  42372  aks4d1p7d1  42373  aks4d1p7  42374  aks4d1p8  42378  aks4d1p9  42379  aks6d1c7lem1  42471  aks6d1c7lem2  42472  aks6d1c7  42475  aks5lem6  42483  aks5lem8  42492  aks5  42495  fzosumm1  42541  dffltz  42913  rmspecnonsq  43185  rmspecfund  43187  rmxyadd  43199  rmxy1  43200  jm2.18  43266  jm2.22  43273  jm2.15nn0  43281  jm2.16nn0  43282  jm2.27a  43283  jm2.27c  43285  jm3.1lem2  43296  jm3.1lem3  43297  jm3.1  43298  expdiophlem1  43299  dvgrat  44589  cvgdvgrat  44590  hashnzfz  44597  uzwo4  45334  ssinc  45367  ssdec  45368  rexanuz3  45376  monoords  45581  fzdifsuc2  45594  iuneqfzuzlem  45615  eluzelzd  45655  allbutfi  45673  eluzelz2  45683  uzid2  45685  monoordxrv  45761  monoord2xrv  45763  fmul01  45862  fmul01lt1lem1  45866  fmul01lt1lem2  45867  climsuselem1  45889  climsuse  45890  climf  45904  climresmpt  45939  climf2  45946  limsupequzlem  46002  limsupmnfuzlem  46006  limsupre3uzlem  46015  itgsinexp  46235  iblspltprt  46253  itgspltprt  46259  iundjiun  46740  smflimsuplem2  47101  smflimsuplem4  47103  smflimsuplem5  47104  fzopredsuc  47605  m1modmmod  47640  smonoord  47653  iccpartiltu  47704  fmtnoprmfac2lem1  47848  fmtnofac2lem  47850  lighneallem2  47888  lighneallem4a  47890  lighneallem4b  47891  fppr2odd  48013  fpprwpprb  48022  gboge9  48046  nnsum3primesle9  48076  nnsum4primesevenALTV  48083  wtgoldbnnsum4prm  48084  bgoldbnnsum3prm  48086  bgoldbtbndlem2  48088  gpgusgralem  48338  gpgprismgr4cycllem9  48385  fllogbd  48842  fllog2  48850  dignn0ldlem  48884  dignnld  48885  digexp  48889  dignn0flhalf  48900  nn0sumshdiglemB  48902