Theorem eluzelz 12913

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573   ≤ cle 11325  ℤcz 12639  ℤ_≥cuz 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640  df-uz 12904

This theorem is referenced by:  eluzelre  12914  uztrn  12921  uzneg  12923  uzss  12926  eluzp1l  12930  eluzadd  12932  eluzsub  12933  eluzaddiOLD  12935  eluzsubiOLD  12937  subeluzsub  12940  uzm1  12941  uzin  12943  uzind4  12971  uzwo  12976  uz2mulcl  12991  uzsupss  13005  elfz5  13576  elfzel2  13582  elfzelz  13584  eluzfz2  13592  peano2fzr  13597  fzsplit2  13609  fzopth  13621  ssfzunsn  13630  fzsuc  13631  elfz1uz  13654  uzsplit  13656  uzdisj  13657  fzm1  13664  uznfz  13667  nn0disj  13701  preduz  13707  elfzo3  13733  fzoss2  13744  fzouzsplit  13751  fzoun  13753  eluzgtdifelfzo  13778  fzosplitsnm1  13791  fzofzp1b  13815  elfzonelfzo  13819  fzosplitsn  13825  fzisfzounsn  13829  fldiv4lem1div2uz2  13887  m1modge3gt1  13969  modaddmodup  13985  om2uzlti  14001  om2uzf1oi  14004  uzrdgxfr  14018  fzen2  14020  seqfveq2  14075  seqfeq2  14076  seqshft2  14079  monoord  14083  monoord2  14084  sermono  14085  seqsplit  14086  seqf1olem1  14092  seqf1olem2  14093  seqid  14098  leexp2a  14222  expnlbnd2  14283  expmulnbnd  14284  hashfz  14476  fzsdom2  14477  hashfzo  14478  hashfzp1  14480  seqcoll  14513  swrdfv2  14709  pfxccatin12  14781  rexuz3  15397  r19.2uz  15400  rexuzre  15401  cau4  15405  caubnd2  15406  clim  15540  climrlim2  15593  climshft2  15628  climaddc1  15681  climmulc2  15683  climsubc1  15684  climsubc2  15685  clim2ser  15703  clim2ser2  15704  iserex  15705  climlec2  15707  climub  15710  isercolllem2  15714  isercoll  15716  isercoll2  15717  climcau  15719  caurcvg2  15726  caucvgb  15728  serf0  15729  iseraltlem1  15730  iseraltlem2  15731  iseralt  15733  sumrblem  15759  fsumcvg  15760  summolem2a  15763  fsumcvg2  15775  fsumm1  15799  fzosump1  15800  fsump1  15804  fsumrev2  15830  telfsumo  15850  fsumparts  15854  isumsplit  15888  isumrpcl  15891  isumsup2  15894  cvgrat  15931  mertenslem1  15932  clim2div  15937  prodeq2ii  15959  fprodcvg  15978  prodmolem2a  15982  zprod  15985  fprodntriv  15990  fprodser  15997  fprodm1  16015  fprodp1  16017  fprodeq0  16023  isprm3  16730  nprm  16735  dvdsprm  16750  exprmfct  16751  isprm5  16754  maxprmfct  16756  prmdvdsncoprmbd  16774  ncoprmlnprm  16775  phibndlem  16817  dfphi2  16821  hashdvds  16822  pcaddlem  16935  pcfac  16946  expnprm  16949  prmreclem4  16966  vdwlem8  17035  gsumval2a  18723  efgs1b  19778  telgsumfzs  20031  iscau4  25332  caucfil  25336  iscmet3lem3  25343  iscmet3lem1  25344  iscmet3lem2  25345  lmle  25354  uniioombllem3  25639  mbflimsup  25720  mbfi1fseqlem6  25775  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  aaliou3lem1  26402  aaliou3lem2  26403  ulmres  26449  ulmshftlem  26450  ulmshft  26451  ulmcaulem  26455  ulmcau  26456  ulmdvlem1  26461  radcnvlem1  26474  logblt  26845  logbgcd1irr  26855  muval1  27194  chtdif  27219  ppidif  27224  chtub  27274  bcmono  27339  bpos1lem  27344  lgsquad2lem2  27447  2sqlem6  27485  2sqlem8a  27487  2sqlem8  27488  chebbnd1lem1  27531  dchrisumlem2  27552  dchrisum0lem1  27578  ostthlem2  27690  ostth2  27699  axlowdimlem3  28977  axlowdimlem6  28980  axlowdimlem7  28981  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  clwwnrepclwwn  30376  fzspl  32795  fzdif2  32796  supfz  35691  divcnvlin  35695  nn0prpwlem  36288  fdc  37705  mettrifi  37717  caushft  37721  aks4d1lem1  42019  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  aks6d1c7lem1  42137  aks6d1c7lem2  42138  aks6d1c7  42141  aks5lem6  42149  aks5lem8  42158  aks5  42161  fzosumm1  42245  dffltz  42589  rmspecnonsq  42863  rmspecfund  42865  rmxyadd  42878  rmxy1  42879  jm2.18  42945  jm2.22  42952  jm2.15nn0  42960  jm2.16nn0  42961  jm2.27a  42962  jm2.27c  42964  jm3.1lem2  42975  jm3.1lem3  42976  jm3.1  42977  expdiophlem1  42978  dvgrat  44281  cvgdvgrat  44282  hashnzfz  44289  uzwo4  44955  ssinc  44989  ssdec  44990  rexanuz3  44998  monoords  45212  fzdifsuc2  45225  iuneqfzuzlem  45249  eluzelzd  45290  allbutfi  45308  eluzelz2  45318  uzid2  45320  monoordxrv  45397  monoord2xrv  45399  fmul01  45501  fmul01lt1lem1  45505  fmul01lt1lem2  45506  climsuselem1  45528  climsuse  45529  climf  45543  climresmpt  45580  climf2  45587  limsupequzlem  45643  limsupmnfuzlem  45647  limsupre3uzlem  45656  itgsinexp  45876  iblspltprt  45894  itgspltprt  45900  iundjiun  46381  smflimsuplem2  46742  smflimsuplem4  46744  smflimsuplem5  46745  fzopredsuc  47238  smonoord  47245  iccpartiltu  47296  fmtnoprmfac2lem1  47440  fmtnofac2lem  47442  lighneallem2  47480  lighneallem4a  47482  lighneallem4b  47483  fppr2odd  47605  fpprwpprb  47614  gboge9  47638  nnsum3primesle9  47668  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  m1modmmod  48255  fllogbd  48294  fllog2  48302  dignn0ldlem  48336  dignnld  48337  digexp  48341  dignn0flhalf  48352  nn0sumshdiglemB  48354