Theorem eluzelz 12985

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5105  ‘cfv 6546   ≤ cle 11354  ℤcz 12703  ℤ_≥cuz 12975

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  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 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-neg 11554  df-z 12704  df-uz 12976

This theorem is used by:  eluzelre  12986  uztrn  12993  uzneg  12995  uzss  12998  eluzp1l  13002  eluzadd  13004  eluzsub  13005  subeluzsub  13008  uzm1  13009  uzin  13011  uzind4  13043  uzwo  13048  uz2mulcl  13063  uzsupss  13077  elfz5  13658  elfzel2  13664  elfzelz  13666  eluzfz2  13675  peano2fzr  13680  fzsplit2  13693  fzopth  13705  ssfzunsn  13714  fzsuc  13715  elfz1uz  13738  uzsplit  13740  uzdisj  13741  fzm1  13751  uznfz  13754  nn0disj  13788  preduz  13794  elfzo3  13821  fzoss2  13832  fzouzsplit  13839  fzoun  13841  eluzgtdifelfzo  13872  fzosplitsnm1  13885  fzofzp1b  13910  elfzonelfzo  13914  fzosplitsn  13921  fzisfzounsn  13925  fldiv4lem1div2uz2  13986  m1modge3gt1  14071  modaddmodup  14087  om2uzlti  14103  om2uzf1oi  14106  uzrdgxfr  14120  fzen2  14122  seqfveq2  14177  seqfeq2  14178  seqshft2  14181  monoord  14185  monoord2  14186  sermono  14187  seqsplit  14188  seqf1olem1  14194  seqf1olem2  14195  seqid  14200  leexp2a  14325  expnlbnd2  14388  expmulnbnd  14389  hashfz  14582  fzsdom2  14583  hashfzo  14584  hashfzp1  14586  seqcoll  14619  swrdfv2  14822  pfxccatin12  14893  rexuz3  15528  r19.2uz  15531  rexuzre  15532  cau4  15536  caubnd2  15537  clim  15673  climrlim2  15726  climshft2  15761  climaddc1  15814  climmulc2  15816  climsubc1  15817  climsubc2  15818  clim2ser  15834  clim2ser2  15835  iserex  15836  climlec2  15838  climub  15841  isercolllem2  15845  isercoll  15847  isercoll2  15848  climcau  15850  caurcvg2  15857  caucvgb  15859  serf0  15860  iseraltlem1  15861  iseraltlem2  15862  iseralt  15864  sumrblem  15889  fsumcvg  15890  summolem2a  15893  fsumcvg2  15905  fsumm1  15929  fzosump1  15930  fsump1  15934  fsumrev2  15960  telfsumo  15981  fsumparts  15985  isumsplit  16021  isumrpcl  16024  isumsup2  16027  cvgrat  16064  mertenslem1  16065  clim2div  16070  prodeq2ii  16092  fprodcvg  16109  prodmolem2a  16113  zprod  16116  fprodntriv  16121  fprodser  16128  fprodm1  16146  fprodp1  16148  fprodeq0  16154  isprm3  16870  nprm  16875  dvdsprm  16891  exprmfct  16892  isprm5  16895  maxprmfct  16897  prmdvdsncoprmbd  16915  ncoprmlnprm  16916  phibndlem  16959  dfphi2  16963  hashdvds  16964  pcaddlem  17078  pcfac  17089  expnprm  17092  prmreclem4  17109  vdwlem8  17178  gsumval2a  18886  efgs1b  19962  telgsumfzs  20215  iscau4  25612  caucfil  25616  iscmet3lem3  25623  iscmet3lem1  25624  iscmet3lem2  25625  lmle  25634  uniioombllem3  25918  mbflimsup  25999  mbfi1fseqlem6  26053  dvfsumle  26353  dvfsumge  26354  dvfsumabs  26355  aaliou3lem1  26681  aaliou3lem2  26682  ulmres  26727  ulmshftlem  26728  ulmshft  26729  ulmcaulem  26733  ulmcau  26734  ulmdvlem1  26739  radcnvlem1  26752  logblt  27124  logbgcd1irr  27134  muval1  27472  chtdif  27497  ppidif  27502  chtub  27551  bcmono  27616  bpos1lem  27621  lgsquad2lem2  27724  2sqlem6  27762  2sqlem8a  27764  2sqlem8  27765  chebbnd1lem1  27808  dchrisumlem2  27829  dchrisum0lem1  27855  ostthlem2  27967  ostth2  27976  axlowdimlem3  29534  axlowdimlem6  29537  axlowdimlem7  29538  axlowdimlem16  29547  axlowdimlem17  29548  axlowdim  29551  clwwnrepclwwn  30957  fzspl  33434  fzdif2  33435  supfz  36621  divcnvlin  36625  nn0prpwlem  37237  fdc  38819  mettrifi  38831  caushft  38835  aks4d1lem1  43252  aks4d1p1  43266  aks4d1p2  43267  aks4d1p3  43268  aks4d1p5  43270  aks4d1p6  43271  aks4d1p7d1  43272  aks4d1p7  43273  aks4d1p8  43277  aks4d1p9  43278  aks6d1c7lem1  43370  aks6d1c7lem2  43371  aks6d1c7  43374  aks5lem6  43382  aks5lem8  43391  aks5  43394  fzosumm1  43441  dffltz  43810  rmspecnonsq  44054  rmspecfund  44056  rmxyadd  44068  rmxy1  44069  jm2.18  44135  jm2.22  44142  jm2.15nn0  44150  jm2.16nn0  44151  jm2.27a  44152  jm2.27c  44154  jm3.1lem2  44165  jm3.1lem3  44166  jm3.1  44167  expdiophlem1  44168  dvgrat  45436  cvgdvgrat  45437  hashnzfz  45444  uzwo4  46209  ssinc  46241  ssdec  46242  rexanuz3  46250  monoords  46452  fzdifsuc2  46465  iuneqfzuzlem  46485  eluzelzd  46525  allbutfi  46543  eluzelz2  46552  uzid2  46554  monoordxrv  46630  monoord2xrv  46632  fmul01  46731  fmul01lt1lem1  46735  fmul01lt1lem2  46736  climsuselem1  46758  climsuse  46759  climf  46773  climresmpt  46808  climf2  46815  limsupequzlem  46871  limsupmnfuzlem  46875  limsupre3uzlem  46884  itgsinexp  47104  iblspltprt  47122  itgspltprt  47128  iundjiun  47609  smflimsuplem2  47970  smflimsuplem4  47972  smflimsuplem5  47973  fzopredsuc  48533  m1modmmod  48573  smonoord  48586  2timesltsq  48587  2timesltsqm1  48588  iccpartiltu  48643  nprmmul1  48748  fmtnoprmfac2lem1  48790  fmtnofac2lem  48792  lighneallem2  48830  lighneallem4a  48832  lighneallem4b  48833  nprmdvdsfacm1lem1  48844  nprmdvdsfacm1lem4  48847  ppivalnnprm  48849  ppivalnnnprmge6  48850  ppivalnn  48856  fppr2odd  48968  fpprwpprb  48977  gboge9  49001  nnsum3primesle9  49031  nnsum4primesevenALTV  49038  wtgoldbnnsum4prm  49039  bgoldbnnsum3prm  49041  bgoldbtbndlem2  49043  gpgusgralem  49293  gpgprismgr4cycllem9  49340  fllogbd  49811  fllog2  49819  dignn0ldlem  49853  dignnld  49854  digexp  49858  dignn0flhalf  49869  nn0sumshdiglemB  49871