Theorem eluzelz 12882

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5112  ‘cfv 6540   ≤ cle 11254  ℤcz 12601  ℤ_≥cuz 12872

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pr 5407  ax-cnex 11166  ax-resscn 11167

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-br 5113  df-opab 5177  df-mpt 5196  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7419  df-neg 11454  df-z 12602  df-uz 12873

This theorem is used by:  eluzelre  12883  uztrn  12890  uzneg  12892  uzss  12895  eluzp1l  12899  eluzadd  12901  eluzsub  12902  subeluzsub  12905  uzm1  12906  uzin  12908  uzind4  12940  uzwo  12945  uz2mulcl  12960  uzsupss  12974  elfz5  13554  elfzel2  13560  elfzelz  13562  eluzfz2  13570  peano2fzr  13575  fzsplit2  13588  fzopth  13600  ssfzunsn  13609  fzsuc  13610  elfz1uz  13633  uzsplit  13635  uzdisj  13636  fzm1  13646  uznfz  13649  nn0disj  13683  preduz  13689  elfzo3  13716  fzoss2  13727  fzouzsplit  13734  fzoun  13736  eluzgtdifelfzo  13767  fzosplitsnm1  13780  fzofzp1b  13805  elfzonelfzo  13809  fzosplitsn  13816  fzisfzounsn  13820  fldiv4lem1div2uz2  13880  m1modge3gt1  13965  modaddmodup  13981  om2uzlti  13997  om2uzf1oi  14000  uzrdgxfr  14014  fzen2  14016  seqfveq2  14071  seqfeq2  14072  seqshft2  14075  monoord  14079  monoord2  14080  sermono  14081  seqsplit  14082  seqf1olem1  14088  seqf1olem2  14089  seqid  14094  leexp2a  14219  expnlbnd2  14281  expmulnbnd  14282  hashfz  14475  fzsdom2  14476  hashfzo  14477  hashfzp1  14479  seqcoll  14512  swrdfv2  14710  pfxccatin12  14781  rexuz3  15411  r19.2uz  15414  rexuzre  15415  cau4  15419  caubnd2  15420  clim  15556  climrlim2  15609  climshft2  15644  climaddc1  15697  climmulc2  15699  climsubc1  15700  climsubc2  15701  clim2ser  15717  clim2ser2  15718  iserex  15719  climlec2  15721  climub  15724  isercolllem2  15728  isercoll  15730  isercoll2  15731  climcau  15733  caurcvg2  15740  caucvgb  15742  serf0  15743  iseraltlem1  15744  iseraltlem2  15745  iseralt  15747  sumrblem  15773  fsumcvg  15774  summolem2a  15777  fsumcvg2  15789  fsumm1  15813  fzosump1  15814  fsump1  15818  fsumrev2  15844  telfsumo  15865  fsumparts  15869  isumsplit  15905  isumrpcl  15908  isumsup2  15911  cvgrat  15948  mertenslem1  15949  clim2div  15954  prodeq2ii  15976  fprodcvg  15995  prodmolem2a  15999  zprod  16002  fprodntriv  16007  fprodser  16014  fprodm1  16032  fprodp1  16034  fprodeq0  16040  isprm3  16751  nprm  16756  dvdsprm  16772  exprmfct  16773  isprm5  16776  maxprmfct  16778  prmdvdsncoprmbd  16796  ncoprmlnprm  16797  phibndlem  16839  dfphi2  16843  hashdvds  16844  pcaddlem  16958  pcfac  16969  expnprm  16972  prmreclem4  16989  vdwlem8  17058  gsumval2a  18753  efgs1b  19816  telgsumfzs  20069  iscau4  25453  caucfil  25457  iscmet3lem3  25464  iscmet3lem1  25465  iscmet3lem2  25466  lmle  25475  uniioombllem3  25759  mbflimsup  25840  mbfi1fseqlem6  25894  dvfsumle  26195  dvfsumge  26196  dvfsumabs  26197  aaliou3lem1  26520  aaliou3lem2  26521  ulmres  26566  ulmshftlem  26567  ulmshft  26568  ulmcaulem  26572  ulmcau  26573  ulmdvlem1  26578  radcnvlem1  26591  logblt  26964  logbgcd1irr  26974  muval1  27312  chtdif  27337  ppidif  27342  chtub  27391  bcmono  27456  bpos1lem  27461  lgsquad2lem2  27564  2sqlem6  27602  2sqlem8a  27604  2sqlem8  27605  chebbnd1lem1  27648  dchrisumlem2  27669  dchrisum0lem1  27695  ostthlem2  27807  ostth2  27816  axlowdimlem3  29309  axlowdimlem6  29312  axlowdimlem7  29313  axlowdimlem16  29322  axlowdimlem17  29323  axlowdim  29326  clwwnrepclwwn  30710  fzspl  33149  fzdif2  33150  supfz  36233  divcnvlin  36237  nn0prpwlem  36865  fdc  38428  mettrifi  38440  caushft  38444  aks4d1lem1  42861  aks4d1p1  42875  aks4d1p2  42876  aks4d1p3  42877  aks4d1p5  42879  aks4d1p6  42880  aks4d1p7d1  42881  aks4d1p7  42882  aks4d1p8  42886  aks4d1p9  42887  aks6d1c7lem1  42979  aks6d1c7lem2  42980  aks6d1c7  42983  aks5lem6  42991  aks5lem8  43000  aks5  43003  fzosumm1  43050  dffltz  43398  rmspecnonsq  43666  rmspecfund  43668  rmxyadd  43680  rmxy1  43681  jm2.18  43747  jm2.22  43754  jm2.15nn0  43762  jm2.16nn0  43763  jm2.27a  43764  jm2.27c  43766  jm3.1lem2  43777  jm3.1lem3  43778  jm3.1  43779  expdiophlem1  43780  dvgrat  45054  cvgdvgrat  45055  hashnzfz  45062  uzwo4  45805  ssinc  45837  ssdec  45838  rexanuz3  45846  monoords  46048  fzdifsuc2  46061  iuneqfzuzlem  46082  eluzelzd  46122  allbutfi  46140  eluzelz2  46149  uzid2  46151  monoordxrv  46227  monoord2xrv  46229  fmul01  46328  fmul01lt1lem1  46332  fmul01lt1lem2  46333  climsuselem1  46355  climsuse  46356  climf  46370  climresmpt  46405  climf2  46412  limsupequzlem  46468  limsupmnfuzlem  46472  limsupre3uzlem  46481  itgsinexp  46701  iblspltprt  46719  itgspltprt  46725  iundjiun  47206  smflimsuplem2  47567  smflimsuplem4  47569  smflimsuplem5  47570  fzopredsuc  48093  m1modmmod  48133  smonoord  48146  2timesltsq  48147  2timesltsqm1  48148  iccpartiltu  48203  nprmmul1  48308  fmtnoprmfac2lem1  48350  fmtnofac2lem  48352  lighneallem2  48390  lighneallem4a  48392  lighneallem4b  48393  nprmdvdsfacm1lem1  48404  nprmdvdsfacm1lem4  48407  ppivalnnprm  48409  ppivalnnnprmge6  48410  ppivalnn  48416  fppr2odd  48528  fpprwpprb  48537  gboge9  48561  nnsum3primesle9  48591  nnsum4primesevenALTV  48598  wtgoldbnnsum4prm  48599  bgoldbnnsum3prm  48601  bgoldbtbndlem2  48603  gpgusgralem  48853  gpgprismgr4cycllem9  48900  fllogbd  49372  fllog2  49380  dignn0ldlem  49414  dignnld  49415  digexp  49419  dignn0flhalf  49430  nn0sumshdiglemB  49432