Theorem eluzelz 12601

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  ‘cfv 6437   ≤ cle 11019  ℤcz 12328  ℤ_≥cuz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-cnex 10936  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329  df-uz 12592

This theorem is referenced by:  eluzelre  12602  uztrn  12609  uzneg  12611  uzss  12614  eluzp1l  12618  eluzaddi  12620  eluzsubi  12621  subeluzsub  12624  uzm1  12625  uzin  12627  uzind4  12655  uzwo  12660  uz2mulcl  12675  uzsupss  12689  elfz5  13257  elfzel2  13263  elfzelz  13265  eluzfz2  13273  peano2fzr  13278  fzsplit2  13290  fzopth  13302  ssfzunsn  13311  fzsuc  13312  elfz1uz  13335  uzsplit  13337  uzdisj  13338  fzm1  13345  uznfz  13348  nn0disj  13381  preduz  13387  elfzo3  13413  fzoss2  13424  fzouzsplit  13431  fzoun  13433  eluzgtdifelfzo  13458  fzosplitsnm1  13471  fzofzp1b  13494  elfzonelfzo  13498  fzosplitsn  13504  fzisfzounsn  13508  fldiv4lem1div2uz2  13565  m1modge3gt1  13647  modaddmodup  13663  om2uzlti  13679  om2uzf1oi  13682  uzrdgxfr  13696  fzen2  13698  seqfveq2  13754  seqfeq2  13755  seqshft2  13758  monoord  13762  monoord2  13763  sermono  13764  seqsplit  13765  seqf1olem1  13771  seqf1olem2  13772  seqid  13777  leexp2a  13899  expnlbnd2  13958  expmulnbnd  13959  hashfz  14151  fzsdom2  14152  hashfzo  14153  hashfzp1  14155  seqcoll  14187  swrdfv2  14383  pfxccatin12  14455  rexuz3  15069  r19.2uz  15072  rexuzre  15073  cau4  15077  caubnd2  15078  clim  15212  climrlim2  15265  climshft2  15300  climaddc1  15353  climmulc2  15355  climsubc1  15356  climsubc2  15357  clim2ser  15375  clim2ser2  15376  iserex  15377  climlec2  15379  climub  15382  isercolllem2  15386  isercoll  15388  isercoll2  15389  climcau  15391  caurcvg2  15398  caucvgb  15400  serf0  15401  iseraltlem1  15402  iseraltlem2  15403  iseralt  15405  sumrblem  15432  fsumcvg  15433  summolem2a  15436  fsumcvg2  15448  fsumm1  15472  fzosump1  15473  fsump1  15477  fsumrev2  15503  telfsumo  15523  fsumparts  15527  isumsplit  15561  isumrpcl  15564  isumsup2  15567  cvgrat  15604  mertenslem1  15605  clim2div  15610  prodeq2ii  15632  fprodcvg  15649  prodmolem2a  15653  zprod  15656  fprodntriv  15661  fprodser  15668  fprodm1  15686  fprodp1  15688  fprodeq0  15694  isprm3  16397  nprm  16402  dvdsprm  16417  exprmfct  16418  isprm5  16421  maxprmfct  16423  prmdvdsncoprmbd  16440  ncoprmlnprm  16441  phibndlem  16480  dfphi2  16484  hashdvds  16485  pcaddlem  16598  pcfac  16609  expnprm  16612  prmreclem4  16629  vdwlem8  16698  gsumval2a  18378  efgs1b  19351  telgsumfzs  19599  iscau4  24452  caucfil  24456  iscmet3lem3  24463  iscmet3lem1  24464  iscmet3lem2  24465  lmle  24474  uniioombllem3  24758  mbflimsup  24839  mbfi1fseqlem6  24894  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  aaliou3lem1  25511  aaliou3lem2  25512  ulmres  25556  ulmshftlem  25557  ulmshft  25558  ulmcaulem  25562  ulmcau  25563  ulmdvlem1  25568  radcnvlem1  25581  logblt  25943  logbgcd1irr  25953  muval1  26291  chtdif  26316  ppidif  26321  chtub  26369  bcmono  26434  bpos1lem  26439  lgsquad2lem2  26542  2sqlem6  26580  2sqlem8a  26582  2sqlem8  26583  chebbnd1lem1  26626  dchrisumlem2  26647  dchrisum0lem1  26673  ostthlem2  26785  ostth2  26794  axlowdimlem3  27321  axlowdimlem6  27324  axlowdimlem7  27325  axlowdimlem16  27334  axlowdimlem17  27335  axlowdim  27338  clwwnrepclwwn  28717  fzspl  31120  fzdif2  31121  supfz  33703  divcnvlin  33707  nn0prpwlem  34520  fdc  35912  mettrifi  35924  caushft  35928  aks4d1lem1  40077  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  fzosumm1  40225  dffltz  40478  rmspecnonsq  40736  rmspecfund  40738  rmxyadd  40750  rmxy1  40751  jm2.18  40817  jm2.22  40824  jm2.15nn0  40832  jm2.16nn0  40833  jm2.27a  40834  jm2.27c  40836  jm3.1lem2  40847  jm3.1lem3  40848  jm3.1  40849  expdiophlem1  40850  dvgrat  41937  cvgdvgrat  41938  hashnzfz  41945  uzwo4  42608  ssinc  42644  ssdec  42645  rexanuz3  42653  monoords  42843  fzdifsuc2  42856  iuneqfzuzlem  42880  eluzelzd  42921  allbutfi  42940  eluzelz2  42950  uzid2  42952  monoordxrv  43029  monoord2xrv  43031  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  climsuselem1  43155  climsuse  43156  climf  43170  climresmpt  43207  climf2  43214  limsupequzlem  43270  limsupmnfuzlem  43274  limsupre3uzlem  43283  itgsinexp  43503  iblspltprt  43521  itgspltprt  43527  iundjiun  44005  smflimsuplem2  44365  smflimsuplem4  44367  smflimsuplem5  44368  fzopredsuc  44826  smonoord  44834  iccpartiltu  44885  fmtnoprmfac2lem1  45029  fmtnofac2lem  45031  lighneallem2  45069  lighneallem4a  45071  lighneallem4b  45072  fppr2odd  45194  fpprwpprb  45203  gboge9  45227  nnsum3primesle9  45257  nnsum4primesevenALTV  45264  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem2  45269  m1modmmod  45878  fllogbd  45917  fllog2  45925  dignn0ldlem  45959  dignnld  45960  digexp  45964  dignn0flhalf  45975  nn0sumshdiglemB  45977