Theorem eluzelz 12860

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  ‘cfv 6530   ≤ cle 11268  ℤcz 12586  ℤ_≥cuz 12850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-cnex 11183  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  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 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406  df-neg 11467  df-z 12587  df-uz 12851

This theorem is referenced by:  eluzelre  12861  uztrn  12868  uzneg  12870  uzss  12873  eluzp1l  12877  eluzadd  12879  eluzsub  12880  eluzaddiOLD  12882  eluzsubiOLD  12884  subeluzsub  12887  uzm1  12888  uzin  12890  uzind4  12920  uzwo  12925  uz2mulcl  12940  uzsupss  12954  elfz5  13531  elfzel2  13537  elfzelz  13539  eluzfz2  13547  peano2fzr  13552  fzsplit2  13564  fzopth  13576  ssfzunsn  13585  fzsuc  13586  elfz1uz  13609  uzsplit  13611  uzdisj  13612  fzm1  13622  uznfz  13625  nn0disj  13659  preduz  13665  elfzo3  13691  fzoss2  13702  fzouzsplit  13709  fzoun  13711  eluzgtdifelfzo  13741  fzosplitsnm1  13754  fzofzp1b  13779  elfzonelfzo  13783  fzosplitsn  13789  fzisfzounsn  13793  fldiv4lem1div2uz2  13851  m1modge3gt1  13934  modaddmodup  13950  om2uzlti  13966  om2uzf1oi  13969  uzrdgxfr  13983  fzen2  13985  seqfveq2  14040  seqfeq2  14041  seqshft2  14044  monoord  14048  monoord2  14049  sermono  14050  seqsplit  14051  seqf1olem1  14057  seqf1olem2  14058  seqid  14063  leexp2a  14188  expnlbnd2  14250  expmulnbnd  14251  hashfz  14443  fzsdom2  14444  hashfzo  14445  hashfzp1  14447  seqcoll  14480  swrdfv2  14677  pfxccatin12  14749  rexuz3  15365  r19.2uz  15368  rexuzre  15369  cau4  15373  caubnd2  15374  clim  15508  climrlim2  15561  climshft2  15596  climaddc1  15649  climmulc2  15651  climsubc1  15652  climsubc2  15653  clim2ser  15669  clim2ser2  15670  iserex  15671  climlec2  15673  climub  15676  isercolllem2  15680  isercoll  15682  isercoll2  15683  climcau  15685  caurcvg2  15692  caucvgb  15694  serf0  15695  iseraltlem1  15696  iseraltlem2  15697  iseralt  15699  sumrblem  15725  fsumcvg  15726  summolem2a  15729  fsumcvg2  15741  fsumm1  15765  fzosump1  15766  fsump1  15770  fsumrev2  15796  telfsumo  15816  fsumparts  15820  isumsplit  15854  isumrpcl  15857  isumsup2  15860  cvgrat  15897  mertenslem1  15898  clim2div  15903  prodeq2ii  15925  fprodcvg  15944  prodmolem2a  15948  zprod  15951  fprodntriv  15956  fprodser  15963  fprodm1  15981  fprodp1  15983  fprodeq0  15989  isprm3  16700  nprm  16705  dvdsprm  16720  exprmfct  16721  isprm5  16724  maxprmfct  16726  prmdvdsncoprmbd  16744  ncoprmlnprm  16745  phibndlem  16787  dfphi2  16791  hashdvds  16792  pcaddlem  16906  pcfac  16917  expnprm  16920  prmreclem4  16937  vdwlem8  17006  gsumval2a  18661  efgs1b  19715  telgsumfzs  19968  iscau4  25229  caucfil  25233  iscmet3lem3  25240  iscmet3lem1  25241  iscmet3lem2  25242  lmle  25251  uniioombllem3  25536  mbflimsup  25617  mbfi1fseqlem6  25671  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  aaliou3lem1  26300  aaliou3lem2  26301  ulmres  26347  ulmshftlem  26348  ulmshft  26349  ulmcaulem  26353  ulmcau  26354  ulmdvlem1  26359  radcnvlem1  26372  logblt  26744  logbgcd1irr  26754  muval1  27093  chtdif  27118  ppidif  27123  chtub  27173  bcmono  27238  bpos1lem  27243  lgsquad2lem2  27346  2sqlem6  27384  2sqlem8a  27386  2sqlem8  27387  chebbnd1lem1  27430  dchrisumlem2  27451  dchrisum0lem1  27477  ostthlem2  27589  ostth2  27598  axlowdimlem3  28869  axlowdimlem6  28872  axlowdimlem7  28873  axlowdimlem16  28882  axlowdimlem17  28883  axlowdim  28886  clwwnrepclwwn  30271  fzspl  32712  fzdif2  32713  supfz  35692  divcnvlin  35696  nn0prpwlem  36286  fdc  37715  mettrifi  37727  caushft  37731  aks4d1lem1  42021  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  aks6d1c7lem1  42139  aks6d1c7lem2  42140  aks6d1c7  42143  aks5lem6  42151  aks5lem8  42160  aks5  42163  fzosumm1  42248  dffltz  42604  rmspecnonsq  42877  rmspecfund  42879  rmxyadd  42892  rmxy1  42893  jm2.18  42959  jm2.22  42966  jm2.15nn0  42974  jm2.16nn0  42975  jm2.27a  42976  jm2.27c  42978  jm3.1lem2  42989  jm3.1lem3  42990  jm3.1  42991  expdiophlem1  42992  dvgrat  44284  cvgdvgrat  44285  hashnzfz  44292  uzwo4  45025  ssinc  45059  ssdec  45060  rexanuz3  45068  monoords  45274  fzdifsuc2  45287  iuneqfzuzlem  45309  eluzelzd  45350  allbutfi  45368  eluzelz2  45378  uzid2  45380  monoordxrv  45456  monoord2xrv  45458  fmul01  45557  fmul01lt1lem1  45561  fmul01lt1lem2  45562  climsuselem1  45584  climsuse  45585  climf  45599  climresmpt  45636  climf2  45643  limsupequzlem  45699  limsupmnfuzlem  45703  limsupre3uzlem  45712  itgsinexp  45932  iblspltprt  45950  itgspltprt  45956  iundjiun  46437  smflimsuplem2  46798  smflimsuplem4  46800  smflimsuplem5  46801  fzopredsuc  47300  smonoord  47333  iccpartiltu  47384  fmtnoprmfac2lem1  47528  fmtnofac2lem  47530  lighneallem2  47568  lighneallem4a  47570  lighneallem4b  47571  fppr2odd  47693  fpprwpprb  47702  gboge9  47726  nnsum3primesle9  47756  nnsum4primesevenALTV  47763  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  bgoldbtbndlem2  47768  gpgusgralem  48008  gpgprismgr4cycllem9  48050  m1modmmod  48449  fllogbd  48488  fllog2  48496  dignn0ldlem  48530  dignnld  48531  digexp  48535  dignn0flhalf  48546  nn0sumshdiglemB  48548