Theorem eluzelz 12867

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536   ≤ cle 11239  ℤcz 12586  ℤ_≥cuz 12857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587  df-uz 12858

This theorem is referenced by:  eluzelre  12868  uztrn  12875  uzneg  12877  uzss  12880  eluzp1l  12884  eluzadd  12886  eluzsub  12887  subeluzsub  12890  uzm1  12891  uzin  12893  uzind4  12925  uzwo  12930  uz2mulcl  12945  uzsupss  12959  elfz5  13539  elfzel2  13545  elfzelz  13547  eluzfz2  13555  peano2fzr  13560  fzsplit2  13573  fzopth  13585  ssfzunsn  13594  fzsuc  13595  elfz1uz  13618  uzsplit  13620  uzdisj  13621  fzm1  13631  uznfz  13634  nn0disj  13668  preduz  13674  elfzo3  13701  fzoss2  13712  fzouzsplit  13719  fzoun  13721  eluzgtdifelfzo  13752  fzosplitsnm1  13765  fzofzp1b  13790  elfzonelfzo  13794  fzosplitsn  13801  fzisfzounsn  13805  fldiv4lem1div2uz2  13865  m1modge3gt1  13950  modaddmodup  13966  om2uzlti  13982  om2uzf1oi  13985  uzrdgxfr  13999  fzen2  14001  seqfveq2  14056  seqfeq2  14057  seqshft2  14060  monoord  14064  monoord2  14065  sermono  14066  seqsplit  14067  seqf1olem1  14073  seqf1olem2  14074  seqid  14079  leexp2a  14204  expnlbnd2  14266  expmulnbnd  14267  hashfz  14460  fzsdom2  14461  hashfzo  14462  hashfzp1  14464  seqcoll  14497  swrdfv2  14695  pfxccatin12  14766  rexuz3  15396  r19.2uz  15399  rexuzre  15400  cau4  15404  caubnd2  15405  clim  15541  climrlim2  15594  climshft2  15629  climaddc1  15682  climmulc2  15684  climsubc1  15685  climsubc2  15686  clim2ser  15702  clim2ser2  15703  iserex  15704  climlec2  15706  climub  15709  isercolllem2  15713  isercoll  15715  isercoll2  15716  climcau  15718  caurcvg2  15725  caucvgb  15727  serf0  15728  iseraltlem1  15729  iseraltlem2  15730  iseralt  15732  sumrblem  15758  fsumcvg  15759  summolem2a  15762  fsumcvg2  15774  fsumm1  15798  fzosump1  15799  fsump1  15803  fsumrev2  15829  telfsumo  15850  fsumparts  15854  isumsplit  15890  isumrpcl  15893  isumsup2  15896  cvgrat  15933  mertenslem1  15934  clim2div  15939  prodeq2ii  15961  fprodcvg  15980  prodmolem2a  15984  zprod  15987  fprodntriv  15992  fprodser  15999  fprodm1  16017  fprodp1  16019  fprodeq0  16025  isprm3  16736  nprm  16741  dvdsprm  16757  exprmfct  16758  isprm5  16761  maxprmfct  16763  prmdvdsncoprmbd  16781  ncoprmlnprm  16782  phibndlem  16824  dfphi2  16828  hashdvds  16829  pcaddlem  16943  pcfac  16954  expnprm  16957  prmreclem4  16974  vdwlem8  17043  gsumval2a  18738  efgs1b  19801  telgsumfzs  20054  iscau4  25438  caucfil  25442  iscmet3lem3  25449  iscmet3lem1  25450  iscmet3lem2  25451  lmle  25460  uniioombllem3  25744  mbflimsup  25825  mbfi1fseqlem6  25879  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  aaliou3lem1  26505  aaliou3lem2  26506  ulmres  26551  ulmshftlem  26552  ulmshft  26553  ulmcaulem  26557  ulmcau  26558  ulmdvlem1  26563  radcnvlem1  26576  logblt  26949  logbgcd1irr  26959  muval1  27297  chtdif  27322  ppidif  27327  chtub  27376  bcmono  27441  bpos1lem  27446  lgsquad2lem2  27549  2sqlem6  27587  2sqlem8a  27589  2sqlem8  27590  chebbnd1lem1  27633  dchrisumlem2  27654  dchrisum0lem1  27680  ostthlem2  27792  ostth2  27801  axlowdimlem3  29294  axlowdimlem6  29297  axlowdimlem7  29298  axlowdimlem16  29307  axlowdimlem17  29308  axlowdim  29311  clwwnrepclwwn  30695  fzspl  33134  fzdif2  33135  supfz  36221  divcnvlin  36225  nn0prpwlem  36853  fdc  38416  mettrifi  38428  caushft  38432  aks4d1lem1  42849  aks4d1p1  42863  aks4d1p2  42864  aks4d1p3  42865  aks4d1p5  42867  aks4d1p6  42868  aks4d1p7d1  42869  aks4d1p7  42870  aks4d1p8  42874  aks4d1p9  42875  aks6d1c7lem1  42967  aks6d1c7lem2  42968  aks6d1c7  42971  aks5lem6  42979  aks5lem8  42988  aks5  42991  fzosumm1  43038  dffltz  43386  rmspecnonsq  43654  rmspecfund  43656  rmxyadd  43668  rmxy1  43669  jm2.18  43735  jm2.22  43742  jm2.15nn0  43750  jm2.16nn0  43751  jm2.27a  43752  jm2.27c  43754  jm3.1lem2  43765  jm3.1lem3  43766  jm3.1  43767  expdiophlem1  43768  dvgrat  45042  cvgdvgrat  45043  hashnzfz  45050  uzwo4  45793  ssinc  45825  ssdec  45826  rexanuz3  45834  monoords  46036  fzdifsuc2  46049  iuneqfzuzlem  46070  eluzelzd  46110  allbutfi  46128  eluzelz2  46137  uzid2  46139  monoordxrv  46215  monoord2xrv  46217  fmul01  46316  fmul01lt1lem1  46320  fmul01lt1lem2  46321  climsuselem1  46343  climsuse  46344  climf  46358  climresmpt  46393  climf2  46400  limsupequzlem  46456  limsupmnfuzlem  46460  limsupre3uzlem  46469  itgsinexp  46689  iblspltprt  46707  itgspltprt  46713  iundjiun  47194  smflimsuplem2  47555  smflimsuplem4  47557  smflimsuplem5  47558  fzopredsuc  48081  m1modmmod  48121  smonoord  48134  2timesltsq  48135  2timesltsqm1  48136  iccpartiltu  48191  nprmmul1  48296  fmtnoprmfac2lem1  48338  fmtnofac2lem  48340  lighneallem2  48378  lighneallem4a  48380  lighneallem4b  48381  nprmdvdsfacm1lem1  48392  nprmdvdsfacm1lem4  48395  ppivalnnprm  48397  ppivalnnnprmge6  48398  ppivalnn  48404  fppr2odd  48516  fpprwpprb  48525  gboge9  48549  nnsum3primesle9  48579  nnsum4primesevenALTV  48586  wtgoldbnnsum4prm  48587  bgoldbnnsum3prm  48589  bgoldbtbndlem2  48591  gpgusgralem  48841  gpgprismgr4cycllem9  48888  fllogbd  49360  fllog2  49368  dignn0ldlem  49402  dignnld  49403  digexp  49407  dignn0flhalf  49418  nn0sumshdiglemB  49420