Theorem eluzelz 12763

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  ‘cfv 6492   ≤ cle 11169  ℤcz 12490  ℤ_≥cuz 12753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-neg 11369  df-z 12491  df-uz 12754

This theorem is referenced by:  eluzelre  12764  uztrn  12771  uzneg  12773  uzss  12776  eluzp1l  12780  eluzadd  12782  eluzsub  12783  subeluzsub  12786  uzm1  12787  uzin  12789  uzind4  12821  uzwo  12826  uz2mulcl  12841  uzsupss  12855  elfz5  13434  elfzel2  13440  elfzelz  13442  eluzfz2  13450  peano2fzr  13455  fzsplit2  13467  fzopth  13479  ssfzunsn  13488  fzsuc  13489  elfz1uz  13512  uzsplit  13514  uzdisj  13515  fzm1  13525  uznfz  13528  nn0disj  13562  preduz  13568  elfzo3  13594  fzoss2  13605  fzouzsplit  13612  fzoun  13614  eluzgtdifelfzo  13645  fzosplitsnm1  13658  fzofzp1b  13683  elfzonelfzo  13687  fzosplitsn  13694  fzisfzounsn  13698  fldiv4lem1div2uz2  13758  m1modge3gt1  13843  modaddmodup  13859  om2uzlti  13875  om2uzf1oi  13878  uzrdgxfr  13892  fzen2  13894  seqfveq2  13949  seqfeq2  13950  seqshft2  13953  monoord  13957  monoord2  13958  sermono  13959  seqsplit  13960  seqf1olem1  13966  seqf1olem2  13967  seqid  13972  leexp2a  14097  expnlbnd2  14159  expmulnbnd  14160  hashfz  14352  fzsdom2  14353  hashfzo  14354  hashfzp1  14356  seqcoll  14389  swrdfv2  14587  pfxccatin12  14658  rexuz3  15274  r19.2uz  15277  rexuzre  15278  cau4  15282  caubnd2  15283  clim  15419  climrlim2  15472  climshft2  15507  climaddc1  15560  climmulc2  15562  climsubc1  15563  climsubc2  15564  clim2ser  15580  clim2ser2  15581  iserex  15582  climlec2  15584  climub  15587  isercolllem2  15591  isercoll  15593  isercoll2  15594  climcau  15596  caurcvg2  15603  caucvgb  15605  serf0  15606  iseraltlem1  15607  iseraltlem2  15608  iseralt  15610  sumrblem  15636  fsumcvg  15637  summolem2a  15640  fsumcvg2  15652  fsumm1  15676  fzosump1  15677  fsump1  15681  fsumrev2  15707  telfsumo  15727  fsumparts  15731  isumsplit  15765  isumrpcl  15768  isumsup2  15771  cvgrat  15808  mertenslem1  15809  clim2div  15814  prodeq2ii  15836  fprodcvg  15855  prodmolem2a  15859  zprod  15862  fprodntriv  15867  fprodser  15874  fprodm1  15892  fprodp1  15894  fprodeq0  15900  isprm3  16612  nprm  16617  dvdsprm  16632  exprmfct  16633  isprm5  16636  maxprmfct  16638  prmdvdsncoprmbd  16656  ncoprmlnprm  16657  phibndlem  16699  dfphi2  16703  hashdvds  16704  pcaddlem  16818  pcfac  16829  expnprm  16832  prmreclem4  16849  vdwlem8  16918  gsumval2a  18612  efgs1b  19667  telgsumfzs  19920  iscau4  25237  caucfil  25241  iscmet3lem3  25248  iscmet3lem1  25249  iscmet3lem2  25250  lmle  25259  uniioombllem3  25544  mbflimsup  25625  mbfi1fseqlem6  25679  dvfsumle  25984  dvfsumleOLD  25985  dvfsumge  25986  dvfsumabs  25987  aaliou3lem1  26308  aaliou3lem2  26309  ulmres  26355  ulmshftlem  26356  ulmshft  26357  ulmcaulem  26361  ulmcau  26362  ulmdvlem1  26367  radcnvlem1  26380  logblt  26752  logbgcd1irr  26762  muval1  27101  chtdif  27126  ppidif  27131  chtub  27181  bcmono  27246  bpos1lem  27251  lgsquad2lem2  27354  2sqlem6  27392  2sqlem8a  27394  2sqlem8  27395  chebbnd1lem1  27438  dchrisumlem2  27459  dchrisum0lem1  27485  ostthlem2  27597  ostth2  27606  axlowdimlem3  29019  axlowdimlem6  29022  axlowdimlem7  29023  axlowdimlem16  29032  axlowdimlem17  29033  axlowdim  29036  clwwnrepclwwn  30421  fzspl  32871  fzdif2  32872  supfz  35925  divcnvlin  35929  nn0prpwlem  36518  fdc  37948  mettrifi  37960  caushft  37964  aks4d1lem1  42338  aks4d1p1  42352  aks4d1p2  42353  aks4d1p3  42354  aks4d1p5  42356  aks4d1p6  42357  aks4d1p7d1  42358  aks4d1p7  42359  aks4d1p8  42363  aks4d1p9  42364  aks6d1c7lem1  42456  aks6d1c7lem2  42457  aks6d1c7  42460  aks5lem6  42468  aks5lem8  42477  aks5  42480  fzosumm1  42526  dffltz  42898  rmspecnonsq  43170  rmspecfund  43172  rmxyadd  43184  rmxy1  43185  jm2.18  43251  jm2.22  43258  jm2.15nn0  43266  jm2.16nn0  43267  jm2.27a  43268  jm2.27c  43270  jm3.1lem2  43281  jm3.1lem3  43282  jm3.1  43283  expdiophlem1  43284  dvgrat  44574  cvgdvgrat  44575  hashnzfz  44582  uzwo4  45319  ssinc  45352  ssdec  45353  rexanuz3  45361  monoords  45566  fzdifsuc2  45579  iuneqfzuzlem  45600  eluzelzd  45640  allbutfi  45658  eluzelz2  45668  uzid2  45670  monoordxrv  45746  monoord2xrv  45748  fmul01  45847  fmul01lt1lem1  45851  fmul01lt1lem2  45852  climsuselem1  45874  climsuse  45875  climf  45889  climresmpt  45924  climf2  45931  limsupequzlem  45987  limsupmnfuzlem  45991  limsupre3uzlem  46000  itgsinexp  46220  iblspltprt  46238  itgspltprt  46244  iundjiun  46725  smflimsuplem2  47086  smflimsuplem4  47088  smflimsuplem5  47089  fzopredsuc  47590  m1modmmod  47625  smonoord  47638  iccpartiltu  47689  fmtnoprmfac2lem1  47833  fmtnofac2lem  47835  lighneallem2  47873  lighneallem4a  47875  lighneallem4b  47876  fppr2odd  47998  fpprwpprb  48007  gboge9  48031  nnsum3primesle9  48061  nnsum4primesevenALTV  48068  wtgoldbnnsum4prm  48069  bgoldbnnsum3prm  48071  bgoldbtbndlem2  48073  gpgusgralem  48323  gpgprismgr4cycllem9  48370  fllogbd  48827  fllog2  48835  dignn0ldlem  48869  dignnld  48870  digexp  48874  dignn0flhalf  48885  nn0sumshdiglemB  48887