Theorem eluzelz 12975

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6538   ≤ cle 11344  ℤcz 12693  ℤ_≥cuz 12965

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11256  ax-resscn 11257

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  eluzelre  12976  uztrn  12983  uzneg  12985  uzss  12988  eluzp1l  12992  eluzadd  12994  eluzsub  12995  subeluzsub  12998  uzm1  12999  uzin  13001  uzind4  13033  uzwo  13038  uz2mulcl  13053  uzsupss  13067  elfz5  13648  elfzel2  13654  elfzelz  13656  eluzfz2  13665  peano2fzr  13670  fzsplit2  13683  fzopth  13695  ssfzunsn  13704  fzsuc  13705  elfz1uz  13728  uzsplit  13730  uzdisj  13731  fzm1  13741  uznfz  13744  nn0disj  13778  preduz  13784  elfzo3  13811  fzoss2  13822  fzouzsplit  13829  fzoun  13831  eluzgtdifelfzo  13862  fzosplitsnm1  13875  fzofzp1b  13900  elfzonelfzo  13904  fzosplitsn  13911  fzisfzounsn  13915  fldiv4lem1div2uz2  13976  m1modge3gt1  14061  modaddmodup  14077  om2uzlti  14093  om2uzf1oi  14096  uzrdgxfr  14110  fzen2  14112  seqfveq2  14167  seqfeq2  14168  seqshft2  14171  monoord  14175  monoord2  14176  sermono  14177  seqsplit  14178  seqf1olem1  14184  seqf1olem2  14185  seqid  14190  leexp2a  14315  expnlbnd2  14378  expmulnbnd  14379  hashfz  14572  fzsdom2  14573  hashfzo  14574  hashfzp1  14576  seqcoll  14609  swrdfv2  14811  pfxccatin12  14882  rexuz3  15516  r19.2uz  15519  rexuzre  15520  cau4  15524  caubnd2  15525  clim  15661  climrlim2  15714  climshft2  15749  climaddc1  15802  climmulc2  15804  climsubc1  15805  climsubc2  15806  clim2ser  15822  clim2ser2  15823  iserex  15824  climlec2  15826  climub  15829  isercolllem2  15833  isercoll  15835  isercoll2  15836  climcau  15838  caurcvg2  15845  caucvgb  15847  serf0  15848  iseraltlem1  15849  iseraltlem2  15850  iseralt  15852  sumrblem  15877  fsumcvg  15878  summolem2a  15881  fsumcvg2  15893  fsumm1  15917  fzosump1  15918  fsump1  15922  fsumrev2  15948  telfsumo  15969  fsumparts  15973  isumsplit  16009  isumrpcl  16012  isumsup2  16015  cvgrat  16052  mertenslem1  16053  clim2div  16058  prodeq2ii  16080  fprodcvg  16097  prodmolem2a  16101  zprod  16104  fprodntriv  16109  fprodser  16116  fprodm1  16134  fprodp1  16136  fprodeq0  16142  isprm3  16858  nprm  16863  dvdsprm  16879  exprmfct  16880  isprm5  16883  maxprmfct  16885  prmdvdsncoprmbd  16903  ncoprmlnprm  16904  phibndlem  16947  dfphi2  16951  hashdvds  16952  pcaddlem  17066  pcfac  17077  expnprm  17080  prmreclem4  17097  vdwlem8  17166  gsumval2a  18874  efgs1b  19950  telgsumfzs  20203  iscau4  25600  caucfil  25604  iscmet3lem3  25611  iscmet3lem1  25612  iscmet3lem2  25613  lmle  25622  uniioombllem3  25906  mbflimsup  25987  mbfi1fseqlem6  26041  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  aaliou3lem1  26669  aaliou3lem2  26670  ulmres  26715  ulmshftlem  26716  ulmshft  26717  ulmcaulem  26721  ulmcau  26722  ulmdvlem1  26727  radcnvlem1  26740  logblt  27112  logbgcd1irr  27122  muval1  27460  chtdif  27485  ppidif  27490  chtub  27539  bcmono  27604  bpos1lem  27609  lgsquad2lem2  27712  2sqlem6  27750  2sqlem8a  27752  2sqlem8  27753  chebbnd1lem1  27796  dchrisumlem2  27817  dchrisum0lem1  27843  ostthlem2  27955  ostth2  27964  axlowdimlem3  29522  axlowdimlem6  29525  axlowdimlem7  29526  axlowdimlem16  29535  axlowdimlem17  29536  axlowdim  29539  clwwnrepclwwn  30945  fzspl  33381  fzdif2  33382  supfz  36494  divcnvlin  36498  nn0prpwlem  37110  fdc  38679  mettrifi  38691  caushft  38695  aks4d1lem1  43112  aks4d1p1  43126  aks4d1p2  43127  aks4d1p3  43128  aks4d1p5  43130  aks4d1p6  43131  aks4d1p7d1  43132  aks4d1p7  43133  aks4d1p8  43137  aks4d1p9  43138  aks6d1c7lem1  43230  aks6d1c7lem2  43231  aks6d1c7  43234  aks5lem6  43242  aks5lem8  43251  aks5  43254  fzosumm1  43301  dffltz  43670  rmspecnonsq  43913  rmspecfund  43915  rmxyadd  43927  rmxy1  43928  jm2.18  43994  jm2.22  44001  jm2.15nn0  44009  jm2.16nn0  44010  jm2.27a  44011  jm2.27c  44013  jm3.1lem2  44024  jm3.1lem3  44025  jm3.1  44026  expdiophlem1  44027  dvgrat  45295  cvgdvgrat  45296  hashnzfz  45303  uzwo4  46069  ssinc  46101  ssdec  46102  rexanuz3  46110  monoords  46312  fzdifsuc2  46325  iuneqfzuzlem  46345  eluzelzd  46385  allbutfi  46403  eluzelz2  46412  uzid2  46414  monoordxrv  46490  monoord2xrv  46492  fmul01  46591  fmul01lt1lem1  46595  fmul01lt1lem2  46596  climsuselem1  46618  climsuse  46619  climf  46633  climresmpt  46668  climf2  46675  limsupequzlem  46731  limsupmnfuzlem  46735  limsupre3uzlem  46744  itgsinexp  46964  iblspltprt  46982  itgspltprt  46988  iundjiun  47469  smflimsuplem2  47830  smflimsuplem4  47832  smflimsuplem5  47833  fzopredsuc  48393  m1modmmod  48433  smonoord  48446  2timesltsq  48447  2timesltsqm1  48448  iccpartiltu  48503  nprmmul1  48608  fmtnoprmfac2lem1  48650  fmtnofac2lem  48652  lighneallem2  48690  lighneallem4a  48692  lighneallem4b  48693  nprmdvdsfacm1lem1  48704  nprmdvdsfacm1lem4  48707  ppivalnnprm  48709  ppivalnnnprmge6  48710  ppivalnn  48716  fppr2odd  48828  fpprwpprb  48837  gboge9  48861  nnsum3primesle9  48891  nnsum4primesevenALTV  48898  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  bgoldbtbndlem2  48903  gpgusgralem  49153  gpgprismgr4cycllem9  49200  fllogbd  49671  fllog2  49679  dignn0ldlem  49713  dignnld  49714  digexp  49718  dignn0flhalf  49729  nn0sumshdiglemB  49731