Theorem eluzelz 12890

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  ‘cfv 6540   ≤ cle 11261  ℤcz 12608  ℤ_≥cuz 12880

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 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-cnex 11173  ax-resscn 11174

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-neg 11461  df-z 12609  df-uz 12881

This theorem is used by:  eluzelre  12891  uztrn  12898  uzneg  12900  uzss  12903  eluzp1l  12907  eluzadd  12909  eluzsub  12910  subeluzsub  12913  uzm1  12914  uzin  12916  uzind4  12948  uzwo  12953  uz2mulcl  12968  uzsupss  12982  elfz5  13562  elfzel2  13568  elfzelz  13570  eluzfz2  13578  peano2fzr  13583  fzsplit2  13596  fzopth  13608  ssfzunsn  13617  fzsuc  13618  elfz1uz  13641  uzsplit  13643  uzdisj  13644  fzm1  13654  uznfz  13657  nn0disj  13691  preduz  13697  elfzo3  13724  fzoss2  13735  fzouzsplit  13742  fzoun  13744  eluzgtdifelfzo  13775  fzosplitsnm1  13788  fzofzp1b  13813  elfzonelfzo  13817  fzosplitsn  13824  fzisfzounsn  13828  fldiv4lem1div2uz2  13889  m1modge3gt1  13974  modaddmodup  13990  om2uzlti  14006  om2uzf1oi  14009  uzrdgxfr  14023  fzen2  14025  seqfveq2  14080  seqfeq2  14081  seqshft2  14084  monoord  14088  monoord2  14089  sermono  14090  seqsplit  14091  seqf1olem1  14097  seqf1olem2  14098  seqid  14103  leexp2a  14228  expnlbnd2  14290  expmulnbnd  14291  hashfz  14484  fzsdom2  14485  hashfzo  14486  hashfzp1  14488  seqcoll  14521  swrdfv2  14723  pfxccatin12  14794  rexuz3  15426  r19.2uz  15429  rexuzre  15430  cau4  15434  caubnd2  15435  clim  15571  climrlim2  15624  climshft2  15659  climaddc1  15712  climmulc2  15714  climsubc1  15715  climsubc2  15716  clim2ser  15732  clim2ser2  15733  iserex  15734  climlec2  15736  climub  15739  isercolllem2  15743  isercoll  15745  isercoll2  15746  climcau  15748  caurcvg2  15755  caucvgb  15757  serf0  15758  iseraltlem1  15759  iseraltlem2  15760  iseralt  15762  sumrblem  15787  fsumcvg  15788  summolem2a  15791  fsumcvg2  15803  fsumm1  15827  fzosump1  15828  fsump1  15832  fsumrev2  15858  telfsumo  15879  fsumparts  15883  isumsplit  15919  isumrpcl  15922  isumsup2  15925  cvgrat  15962  mertenslem1  15963  clim2div  15968  prodeq2ii  15990  fprodcvg  16009  prodmolem2a  16013  zprod  16016  fprodntriv  16021  fprodser  16028  fprodm1  16046  fprodp1  16048  fprodeq0  16054  isprm3  16765  nprm  16770  dvdsprm  16786  exprmfct  16787  isprm5  16790  maxprmfct  16792  prmdvdsncoprmbd  16810  ncoprmlnprm  16811  phibndlem  16853  dfphi2  16857  hashdvds  16858  pcaddlem  16972  pcfac  16983  expnprm  16986  prmreclem4  17003  vdwlem8  17072  gsumval2a  18777  efgs1b  19852  telgsumfzs  20105  iscau4  25491  caucfil  25495  iscmet3lem3  25502  iscmet3lem1  25503  iscmet3lem2  25504  lmle  25513  uniioombllem3  25797  mbflimsup  25878  mbfi1fseqlem6  25932  dvfsumle  26233  dvfsumge  26234  dvfsumabs  26235  aaliou3lem1  26558  aaliou3lem2  26559  ulmres  26604  ulmshftlem  26605  ulmshft  26606  ulmcaulem  26610  ulmcau  26611  ulmdvlem1  26616  radcnvlem1  26629  logblt  27002  logbgcd1irr  27012  muval1  27350  chtdif  27375  ppidif  27380  chtub  27429  bcmono  27494  bpos1lem  27499  lgsquad2lem2  27602  2sqlem6  27640  2sqlem8a  27642  2sqlem8  27643  chebbnd1lem1  27686  dchrisumlem2  27707  dchrisum0lem1  27733  ostthlem2  27845  ostth2  27854  axlowdimlem3  29351  axlowdimlem6  29354  axlowdimlem7  29355  axlowdimlem16  29364  axlowdimlem17  29365  axlowdim  29368  clwwnrepclwwn  30768  fzspl  33206  fzdif2  33207  supfz  36260  divcnvlin  36264  nn0prpwlem  36892  fdc  38456  mettrifi  38468  caushft  38472  aks4d1lem1  42889  aks4d1p1  42903  aks4d1p2  42904  aks4d1p3  42905  aks4d1p5  42907  aks4d1p6  42908  aks4d1p7d1  42909  aks4d1p7  42910  aks4d1p8  42914  aks4d1p9  42915  aks6d1c7lem1  43007  aks6d1c7lem2  43008  aks6d1c7  43011  aks5lem6  43019  aks5lem8  43028  aks5  43031  fzosumm1  43078  dffltz  43426  rmspecnonsq  43694  rmspecfund  43696  rmxyadd  43708  rmxy1  43709  jm2.18  43775  jm2.22  43782  jm2.15nn0  43790  jm2.16nn0  43791  jm2.27a  43792  jm2.27c  43794  jm3.1lem2  43805  jm3.1lem3  43806  jm3.1  43807  expdiophlem1  43808  dvgrat  45082  cvgdvgrat  45083  hashnzfz  45090  uzwo4  45833  ssinc  45865  ssdec  45866  rexanuz3  45874  monoords  46076  fzdifsuc2  46089  iuneqfzuzlem  46110  eluzelzd  46150  allbutfi  46168  eluzelz2  46177  uzid2  46179  monoordxrv  46255  monoord2xrv  46257  fmul01  46356  fmul01lt1lem1  46360  fmul01lt1lem2  46361  climsuselem1  46383  climsuse  46384  climf  46398  climresmpt  46433  climf2  46440  limsupequzlem  46496  limsupmnfuzlem  46500  limsupre3uzlem  46509  itgsinexp  46729  iblspltprt  46747  itgspltprt  46753  iundjiun  47234  smflimsuplem2  47595  smflimsuplem4  47597  smflimsuplem5  47598  fzopredsuc  48121  m1modmmod  48161  smonoord  48174  2timesltsq  48175  2timesltsqm1  48176  iccpartiltu  48231  nprmmul1  48336  fmtnoprmfac2lem1  48378  fmtnofac2lem  48380  lighneallem2  48418  lighneallem4a  48420  lighneallem4b  48421  nprmdvdsfacm1lem1  48432  nprmdvdsfacm1lem4  48435  ppivalnnprm  48437  ppivalnnnprmge6  48438  ppivalnn  48444  fppr2odd  48556  fpprwpprb  48565  gboge9  48589  nnsum3primesle9  48619  nnsum4primesevenALTV  48626  wtgoldbnnsum4prm  48627  bgoldbnnsum3prm  48629  bgoldbtbndlem2  48631  gpgusgralem  48881  gpgprismgr4cycllem9  48928  fllogbd  49399  fllog2  49407  dignn0ldlem  49441  dignnld  49442  digexp  49446  dignn0flhalf  49457  nn0sumshdiglemB  49459