Theorem eluzelz 12900

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533   ≤ cle 11271  ℤcz 12618  ℤ_≥cuz 12890

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-cnex 11183  ax-resscn 11184

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-neg 11471  df-z 12619  df-uz 12891

This theorem is used by:  eluzelre  12901  uztrn  12908  uzneg  12910  uzss  12913  eluzp1l  12917  eluzadd  12919  eluzsub  12920  subeluzsub  12923  uzm1  12924  uzin  12926  uzind4  12958  uzwo  12963  uz2mulcl  12978  uzsupss  12992  elfz5  13573  elfzel2  13579  elfzelz  13581  eluzfz2  13589  peano2fzr  13594  fzsplit2  13607  fzopth  13619  ssfzunsn  13628  fzsuc  13629  elfz1uz  13652  uzsplit  13654  uzdisj  13655  fzm1  13665  uznfz  13668  nn0disj  13702  preduz  13708  elfzo3  13735  fzoss2  13746  fzouzsplit  13753  fzoun  13755  eluzgtdifelfzo  13786  fzosplitsnm1  13799  fzofzp1b  13824  elfzonelfzo  13828  fzosplitsn  13835  fzisfzounsn  13839  fldiv4lem1div2uz2  13900  m1modge3gt1  13985  modaddmodup  14001  om2uzlti  14017  om2uzf1oi  14020  uzrdgxfr  14034  fzen2  14036  seqfveq2  14091  seqfeq2  14092  seqshft2  14095  monoord  14099  monoord2  14100  sermono  14101  seqsplit  14102  seqf1olem1  14108  seqf1olem2  14109  seqid  14114  leexp2a  14239  expnlbnd2  14301  expmulnbnd  14302  hashfz  14495  fzsdom2  14496  hashfzo  14497  hashfzp1  14499  seqcoll  14532  swrdfv2  14734  pfxccatin12  14805  rexuz3  15439  r19.2uz  15442  rexuzre  15443  cau4  15447  caubnd2  15448  clim  15584  climrlim2  15637  climshft2  15672  climaddc1  15725  climmulc2  15727  climsubc1  15728  climsubc2  15729  clim2ser  15745  clim2ser2  15746  iserex  15747  climlec2  15749  climub  15752  isercolllem2  15756  isercoll  15758  isercoll2  15759  climcau  15761  caurcvg2  15768  caucvgb  15770  serf0  15771  iseraltlem1  15772  iseraltlem2  15773  iseralt  15775  sumrblem  15800  fsumcvg  15801  summolem2a  15804  fsumcvg2  15816  fsumm1  15840  fzosump1  15841  fsump1  15845  fsumrev2  15871  telfsumo  15892  fsumparts  15896  isumsplit  15932  isumrpcl  15935  isumsup2  15938  cvgrat  15975  mertenslem1  15976  clim2div  15981  prodeq2ii  16003  fprodcvg  16020  prodmolem2a  16024  zprod  16027  fprodntriv  16032  fprodser  16039  fprodm1  16057  fprodp1  16059  fprodeq0  16065  isprm3  16776  nprm  16781  dvdsprm  16797  exprmfct  16798  isprm5  16801  maxprmfct  16803  prmdvdsncoprmbd  16821  ncoprmlnprm  16822  phibndlem  16864  dfphi2  16868  hashdvds  16869  pcaddlem  16983  pcfac  16994  expnprm  16997  prmreclem4  17014  vdwlem8  17083  gsumval2a  18790  efgs1b  19866  telgsumfzs  20119  iscau4  25510  caucfil  25514  iscmet3lem3  25521  iscmet3lem1  25522  iscmet3lem2  25523  lmle  25532  uniioombllem3  25816  mbflimsup  25897  mbfi1fseqlem6  25951  dvfsumle  26251  dvfsumge  26252  dvfsumabs  26253  aaliou3lem1  26581  aaliou3lem2  26582  ulmres  26627  ulmshftlem  26628  ulmshft  26629  ulmcaulem  26633  ulmcau  26634  ulmdvlem1  26639  radcnvlem1  26652  logblt  27024  logbgcd1irr  27034  muval1  27372  chtdif  27397  ppidif  27402  chtub  27451  bcmono  27516  bpos1lem  27521  lgsquad2lem2  27624  2sqlem6  27662  2sqlem8a  27664  2sqlem8  27665  chebbnd1lem1  27708  dchrisumlem2  27729  dchrisum0lem1  27755  ostthlem2  27867  ostth2  27876  axlowdimlem3  29404  axlowdimlem6  29407  axlowdimlem7  29408  axlowdimlem16  29417  axlowdimlem17  29418  axlowdim  29421  clwwnrepclwwn  30827  fzspl  33263  fzdif2  33264  supfz  36311  divcnvlin  36315  nn0prpwlem  36944  fdc  38498  mettrifi  38510  caushft  38514  aks4d1lem1  42931  aks4d1p1  42945  aks4d1p2  42946  aks4d1p3  42947  aks4d1p5  42949  aks4d1p6  42950  aks4d1p7d1  42951  aks4d1p7  42952  aks4d1p8  42956  aks4d1p9  42957  aks6d1c7lem1  43049  aks6d1c7lem2  43050  aks6d1c7  43053  aks5lem6  43061  aks5lem8  43070  aks5  43073  fzosumm1  43120  dffltz  43483  rmspecnonsq  43751  rmspecfund  43753  rmxyadd  43765  rmxy1  43766  jm2.18  43832  jm2.22  43839  jm2.15nn0  43847  jm2.16nn0  43848  jm2.27a  43849  jm2.27c  43851  jm3.1lem2  43862  jm3.1lem3  43863  jm3.1  43864  expdiophlem1  43865  dvgrat  45139  cvgdvgrat  45140  hashnzfz  45147  uzwo4  45890  ssinc  45922  ssdec  45923  rexanuz3  45931  monoords  46133  fzdifsuc2  46146  iuneqfzuzlem  46167  eluzelzd  46207  allbutfi  46225  eluzelz2  46234  uzid2  46236  monoordxrv  46312  monoord2xrv  46314  fmul01  46413  fmul01lt1lem1  46417  fmul01lt1lem2  46418  climsuselem1  46440  climsuse  46441  climf  46455  climresmpt  46490  climf2  46497  limsupequzlem  46553  limsupmnfuzlem  46557  limsupre3uzlem  46566  itgsinexp  46786  iblspltprt  46804  itgspltprt  46810  iundjiun  47291  smflimsuplem2  47652  smflimsuplem4  47654  smflimsuplem5  47655  fzopredsuc  48215  m1modmmod  48255  smonoord  48268  2timesltsq  48269  2timesltsqm1  48270  iccpartiltu  48325  nprmmul1  48430  fmtnoprmfac2lem1  48472  fmtnofac2lem  48474  lighneallem2  48512  lighneallem4a  48514  lighneallem4b  48515  nprmdvdsfacm1lem1  48526  nprmdvdsfacm1lem4  48529  ppivalnnprm  48531  ppivalnnnprmge6  48532  ppivalnn  48538  fppr2odd  48650  fpprwpprb  48659  gboge9  48683  nnsum3primesle9  48713  nnsum4primesevenALTV  48720  wtgoldbnnsum4prm  48721  bgoldbnnsum3prm  48723  bgoldbtbndlem2  48725  gpgusgralem  48975  gpgprismgr4cycllem9  49022  fllogbd  49493  fllog2  49501  dignn0ldlem  49535  dignnld  49536  digexp  49540  dignn0flhalf  49551  nn0sumshdiglemB  49553