Theorem eluzelz 12521

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 12517	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1144	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  ‘cfv 6418   ≤ cle 10941  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  eluzelre  12522  uztrn  12529  uzneg  12531  uzss  12534  eluzp1l  12538  eluzaddi  12540  eluzsubi  12541  subeluzsub  12544  uzm1  12545  uzin  12547  uzind4  12575  uzwo  12580  uz2mulcl  12595  uzsupss  12609  elfz5  13177  elfzel2  13183  elfzelz  13185  eluzfz2  13193  peano2fzr  13198  fzsplit2  13210  fzopth  13222  ssfzunsn  13231  fzsuc  13232  elfz1uz  13255  uzsplit  13257  uzdisj  13258  fzm1  13265  uznfz  13268  nn0disj  13301  preduz  13307  elfzo3  13332  fzoss2  13343  fzouzsplit  13350  fzoun  13352  eluzgtdifelfzo  13377  fzosplitsnm1  13390  fzofzp1b  13413  elfzonelfzo  13417  fzosplitsn  13423  fzisfzounsn  13427  fldiv4lem1div2uz2  13484  m1modge3gt1  13566  modaddmodup  13582  om2uzlti  13598  om2uzf1oi  13601  uzrdgxfr  13615  fzen2  13617  seqfveq2  13673  seqfeq2  13674  seqshft2  13677  monoord  13681  monoord2  13682  sermono  13683  seqsplit  13684  seqf1olem1  13690  seqf1olem2  13691  seqid  13696  leexp2a  13818  expnlbnd2  13877  expmulnbnd  13878  hashfz  14070  fzsdom2  14071  hashfzo  14072  hashfzp1  14074  seqcoll  14106  swrdfv2  14302  pfxccatin12  14374  rexuz3  14988  r19.2uz  14991  rexuzre  14992  cau4  14996  caubnd2  14997  clim  15131  climrlim2  15184  climshft2  15219  climaddc1  15272  climmulc2  15274  climsubc1  15275  climsubc2  15276  clim2ser  15294  clim2ser2  15295  iserex  15296  climlec2  15298  climub  15301  isercolllem2  15305  isercoll  15307  isercoll2  15308  climcau  15310  caurcvg2  15317  caucvgb  15319  serf0  15320  iseraltlem1  15321  iseraltlem2  15322  iseralt  15324  sumrblem  15351  fsumcvg  15352  summolem2a  15355  fsumcvg2  15367  fsumm1  15391  fzosump1  15392  fsump1  15396  fsumrev2  15422  telfsumo  15442  fsumparts  15446  isumsplit  15480  isumrpcl  15483  isumsup2  15486  cvgrat  15523  mertenslem1  15524  clim2div  15529  prodeq2ii  15551  fprodcvg  15568  prodmolem2a  15572  zprod  15575  fprodntriv  15580  fprodser  15587  fprodm1  15605  fprodp1  15607  fprodeq0  15613  isprm3  16316  nprm  16321  dvdsprm  16336  exprmfct  16337  isprm5  16340  maxprmfct  16342  prmdvdsncoprmbd  16359  ncoprmlnprm  16360  phibndlem  16399  dfphi2  16403  hashdvds  16404  pcaddlem  16517  pcfac  16528  expnprm  16531  prmreclem4  16548  vdwlem8  16617  gsumval2a  18284  efgs1b  19257  telgsumfzs  19505  iscau4  24348  caucfil  24352  iscmet3lem3  24359  iscmet3lem1  24360  iscmet3lem2  24361  lmle  24370  uniioombllem3  24654  mbflimsup  24735  mbfi1fseqlem6  24790  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  aaliou3lem1  25407  aaliou3lem2  25408  ulmres  25452  ulmshftlem  25453  ulmshft  25454  ulmcaulem  25458  ulmcau  25459  ulmdvlem1  25464  radcnvlem1  25477  logblt  25839  logbgcd1irr  25849  muval1  26187  chtdif  26212  ppidif  26217  chtub  26265  bcmono  26330  bpos1lem  26335  lgsquad2lem2  26438  2sqlem6  26476  2sqlem8a  26478  2sqlem8  26479  chebbnd1lem1  26522  dchrisumlem2  26543  dchrisum0lem1  26569  ostthlem2  26681  ostth2  26690  axlowdimlem3  27215  axlowdimlem6  27218  axlowdimlem7  27219  axlowdimlem16  27228  axlowdimlem17  27229  axlowdim  27232  clwwnrepclwwn  28609  fzspl  31013  fzdif2  31014  supfz  33600  divcnvlin  33604  nn0prpwlem  34438  fdc  35830  mettrifi  35842  caushft  35846  aks4d1lem1  39998  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  fzosumm1  40144  dffltz  40387  rmspecnonsq  40645  rmspecfund  40647  rmxyadd  40659  rmxy1  40660  jm2.18  40726  jm2.22  40733  jm2.15nn0  40741  jm2.16nn0  40742  jm2.27a  40743  jm2.27c  40745  jm3.1lem2  40756  jm3.1lem3  40757  jm3.1  40758  expdiophlem1  40759  dvgrat  41819  cvgdvgrat  41820  hashnzfz  41827  uzwo4  42490  ssinc  42526  ssdec  42527  rexanuz3  42535  monoords  42726  fzdifsuc2  42739  iuneqfzuzlem  42763  eluzelzd  42804  allbutfi  42823  eluzelz2  42833  uzid2  42835  monoordxrv  42912  monoord2xrv  42914  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  climsuselem1  43038  climsuse  43039  climf  43053  climresmpt  43090  climf2  43097  limsupequzlem  43153  limsupmnfuzlem  43157  limsupre3uzlem  43166  itgsinexp  43386  iblspltprt  43404  itgspltprt  43410  iundjiun  43888  smflimsuplem2  44241  smflimsuplem4  44243  smflimsuplem5  44244  fzopredsuc  44703  smonoord  44711  iccpartiltu  44762  fmtnoprmfac2lem1  44906  fmtnofac2lem  44908  lighneallem2  44946  lighneallem4a  44948  lighneallem4b  44949  fppr2odd  45071  fpprwpprb  45080  gboge9  45104  nnsum3primesle9  45134  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem2  45146  m1modmmod  45755  fllogbd  45794  fllog2  45802  dignn0ldlem  45836  dignnld  45837  digexp  45841  dignn0flhalf  45852  nn0sumshdiglemB  45854