Theorem eluzelz 13015

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  ‘cfv 6566   ≤ cle 11383  ℤcz 12733  ℤ_≥cuz 13005

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-cnex 11295  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-neg 11583  df-z 12734  df-uz 13006

This theorem is used by:  eluzelre  13016  uztrn  13023  uzneg  13025  uzss  13028  eluzp1l  13032  eluzadd  13034  eluzsub  13035  subeluzsub  13038  uzm1  13039  uzin  13041  uzind4  13073  uzwo  13078  uz2mulcl  13093  uzsupss  13107  elfz5  13688  elfzel2  13694  elfzelz  13696  eluzfz2  13705  peano2fzr  13710  fzsplit2  13723  fzopth  13735  ssfzunsn  13744  fzsuc  13745  elfz1uz  13768  uzsplit  13770  uzdisj  13771  fzm1  13781  uznfz  13784  nn0disj  13818  preduz  13824  elfzo3  13851  fzoss2  13862  fzouzsplit  13869  fzoun  13871  eluzgtdifelfzo  13902  fzosplitsnm1  13915  fzofzp1b  13940  elfzonelfzo  13944  fzosplitsn  13951  fzisfzounsn  13955  fldiv4lem1div2uz2  14016  m1modge3gt1  14101  modaddmodup  14117  om2uzlti  14133  om2uzf1oi  14136  uzrdgxfr  14150  fzen2  14152  seqfveq2  14207  seqfeq2  14208  seqshft2  14211  monoord  14215  monoord2  14216  sermono  14217  seqsplit  14218  seqf1olem1  14224  seqf1olem2  14225  seqid  14230  leexp2a  14355  expnlbnd2  14419  expmulnbnd  14420  hashfz  14613  fzsdom2  14614  hashfzo  14615  hashfzp1  14617  seqcoll  14650  swrdfv2  14853  pfxccatin12  14924  rexuz3  15560  r19.2uz  15563  rexuzre  15564  cau4  15568  caubnd2  15569  clim  15705  climrlim2  15758  climshft2  15793  climaddc1  15846  climmulc2  15848  climsubc1  15849  climsubc2  15850  clim2ser  15866  clim2ser2  15867  iserex  15868  climlec2  15870  climub  15873  isercolllem2  15877  isercoll  15879  isercoll2  15880  climcau  15882  caurcvg2  15889  caucvgb  15891  serf0  15892  iseraltlem1  15893  iseraltlem2  15894  iseralt  15896  sumrblem  15921  fsumcvg  15922  summolem2a  15925  fsumcvg2  15937  fsumm1  15961  fzosump1  15962  fsump1  15966  fsumrev2  15992  telfsumo  16013  fsumparts  16017  isumsplit  16053  isumrpcl  16056  isumsup2  16059  cvgrat  16096  mertenslem1  16097  clim2div  16102  prodeq2ii  16124  fprodcvg  16141  prodmolem2a  16145  zprod  16148  fprodntriv  16153  fprodser  16160  fprodm1  16178  fprodp1  16180  fprodeq0  16186  isprm3  16902  nprm  16907  dvdsprm  16923  exprmfct  16924  isprm5  16927  maxprmfct  16929  prmdvdsncoprmbd  16947  ncoprmlnprm  16948  phibndlem  16991  dfphi2  16995  hashdvds  16996  pcaddlem  17110  pcfac  17121  expnprm  17124  prmreclem4  17141  vdwlem8  17210  gsumval2a  18924  efgs1b  20001  telgsumfzs  20254  iscau4  25655  caucfil  25659  iscmet3lem3  25666  iscmet3lem1  25667  iscmet3lem2  25668  lmle  25677  uniioombllem3  25961  mbflimsup  26042  mbfi1fseqlem6  26096  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  aaliou3lem1  26726  aaliou3lem2  26727  ulmres  26772  ulmshftlem  26773  ulmshft  26774  ulmcaulem  26778  ulmcau  26779  ulmdvlem1  26784  radcnvlem1  26797  logblt  27169  logbgcd1irr  27179  muval1  27517  chtdif  27542  ppidif  27547  chtub  27596  bcmono  27661  bpos1lem  27666  lgsquad2lem2  27769  2sqlem6  27807  2sqlem8a  27809  2sqlem8  27810  chebbnd1lem1  27853  dchrisumlem2  27874  dchrisum0lem1  27900  ostthlem2  28012  ostth2  28021  axlowdimlem3  29579  axlowdimlem6  29582  axlowdimlem7  29583  axlowdimlem16  29592  axlowdimlem17  29593  axlowdim  29596  clwwnrepclwwn  31002  fzspl  33477  fzdif2  33478  supfz  36709  divcnvlin  36713  nn0prpwlem  37325  fdc  38945  mettrifi  38957  caushft  38961  aks4d1lem1  43378  aks4d1p1  43392  aks4d1p2  43393  aks4d1p3  43394  aks4d1p5  43396  aks4d1p6  43397  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8  43403  aks4d1p9  43404  aks6d1c7lem1  43496  aks6d1c7lem2  43497  aks6d1c7  43500  aks5lem6  43508  aks5lem8  43517  aks5  43520  fzosumm1  43567  dffltz  43936  rmspecnonsq  44180  rmspecfund  44182  rmxyadd  44194  rmxy1  44195  jm2.18  44261  jm2.22  44268  jm2.15nn0  44276  jm2.16nn0  44277  jm2.27a  44278  jm2.27c  44280  jm3.1lem2  44291  jm3.1lem3  44292  jm3.1  44293  expdiophlem1  44294  dvgrat  45557  cvgdvgrat  45558  hashnzfz  45565  uzwo4  46344  ssinc  46375  ssdec  46376  rexanuz3  46384  monoords  46586  fzdifsuc2  46599  iuneqfzuzlem  46619  eluzelzd  46659  allbutfi  46677  eluzelz2  46686  uzid2  46688  monoordxrv  46764  monoord2xrv  46766  fmul01  46865  fmul01lt1lem1  46869  fmul01lt1lem2  46870  climsuselem1  46892  climsuse  46893  climf  46907  climresmpt  46942  climf2  46949  limsupequzlem  47005  limsupmnfuzlem  47009  limsupre3uzlem  47018  itgsinexp  47238  iblspltprt  47256  itgspltprt  47262  iundjiun  47743  smflimsuplem2  48104  smflimsuplem4  48106  smflimsuplem5  48107  fzopredsuc  48667  m1modmmod  48707  smonoord  48720  2timesltsq  48721  2timesltsqm1  48722  iccpartiltu  48777  nprmmul1  48882  fmtnoprmfac2lem1  48924  fmtnofac2lem  48926  lighneallem2  48964  lighneallem4a  48966  lighneallem4b  48967  nprmdvdsfacm1lem1  48978  nprmdvdsfacm1lem4  48981  ppivalnnprm  48983  ppivalnnnprmge6  48984  ppivalnn  48990  fppr2odd  49102  fpprwpprb  49111  gboge9  49135  nnsum3primesle9  49165  nnsum4primesevenALTV  49172  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  bgoldbtbndlem2  49177  gpgusgralem  49427  gpgprismgr4cycllem9  49474  fllogbd  50003  fllog2  50011  dignn0ldlem  50045  dignnld  50046  digexp  50050  dignn0flhalf  50061  nn0sumshdiglemB  50063