Theorem eluzelz 12759

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  ‘cfv 6490   ≤ cle 11165  ℤcz 12486  ℤ_≥cuz 12749

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-cnex 11080  ax-resscn 11081

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487  df-uz 12750

This theorem is referenced by:  eluzelre  12760  uztrn  12767  uzneg  12769  uzss  12772  eluzp1l  12776  eluzadd  12778  eluzsub  12779  subeluzsub  12782  uzm1  12783  uzin  12785  uzind4  12817  uzwo  12822  uz2mulcl  12837  uzsupss  12851  elfz5  13430  elfzel2  13436  elfzelz  13438  eluzfz2  13446  peano2fzr  13451  fzsplit2  13463  fzopth  13475  ssfzunsn  13484  fzsuc  13485  elfz1uz  13508  uzsplit  13510  uzdisj  13511  fzm1  13521  uznfz  13524  nn0disj  13558  preduz  13564  elfzo3  13590  fzoss2  13601  fzouzsplit  13608  fzoun  13610  eluzgtdifelfzo  13641  fzosplitsnm1  13654  fzofzp1b  13679  elfzonelfzo  13683  fzosplitsn  13690  fzisfzounsn  13694  fldiv4lem1div2uz2  13754  m1modge3gt1  13839  modaddmodup  13855  om2uzlti  13871  om2uzf1oi  13874  uzrdgxfr  13888  fzen2  13890  seqfveq2  13945  seqfeq2  13946  seqshft2  13949  monoord  13953  monoord2  13954  sermono  13955  seqsplit  13956  seqf1olem1  13962  seqf1olem2  13963  seqid  13968  leexp2a  14093  expnlbnd2  14155  expmulnbnd  14156  hashfz  14348  fzsdom2  14349  hashfzo  14350  hashfzp1  14352  seqcoll  14385  swrdfv2  14583  pfxccatin12  14654  rexuz3  15270  r19.2uz  15273  rexuzre  15274  cau4  15278  caubnd2  15279  clim  15415  climrlim2  15468  climshft2  15503  climaddc1  15556  climmulc2  15558  climsubc1  15559  climsubc2  15560  clim2ser  15576  clim2ser2  15577  iserex  15578  climlec2  15580  climub  15583  isercolllem2  15587  isercoll  15589  isercoll2  15590  climcau  15592  caurcvg2  15599  caucvgb  15601  serf0  15602  iseraltlem1  15603  iseraltlem2  15604  iseralt  15606  sumrblem  15632  fsumcvg  15633  summolem2a  15636  fsumcvg2  15648  fsumm1  15672  fzosump1  15673  fsump1  15677  fsumrev2  15703  telfsumo  15723  fsumparts  15727  isumsplit  15761  isumrpcl  15764  isumsup2  15767  cvgrat  15804  mertenslem1  15805  clim2div  15810  prodeq2ii  15832  fprodcvg  15851  prodmolem2a  15855  zprod  15858  fprodntriv  15863  fprodser  15870  fprodm1  15888  fprodp1  15890  fprodeq0  15896  isprm3  16608  nprm  16613  dvdsprm  16628  exprmfct  16629  isprm5  16632  maxprmfct  16634  prmdvdsncoprmbd  16652  ncoprmlnprm  16653  phibndlem  16695  dfphi2  16699  hashdvds  16700  pcaddlem  16814  pcfac  16825  expnprm  16828  prmreclem4  16845  vdwlem8  16914  gsumval2a  18608  efgs1b  19663  telgsumfzs  19916  iscau4  25233  caucfil  25237  iscmet3lem3  25244  iscmet3lem1  25245  iscmet3lem2  25246  lmle  25255  uniioombllem3  25540  mbflimsup  25621  mbfi1fseqlem6  25675  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumabs  25983  aaliou3lem1  26304  aaliou3lem2  26305  ulmres  26351  ulmshftlem  26352  ulmshft  26353  ulmcaulem  26357  ulmcau  26358  ulmdvlem1  26363  radcnvlem1  26376  logblt  26748  logbgcd1irr  26758  muval1  27097  chtdif  27122  ppidif  27127  chtub  27177  bcmono  27242  bpos1lem  27247  lgsquad2lem2  27350  2sqlem6  27388  2sqlem8a  27390  2sqlem8  27391  chebbnd1lem1  27434  dchrisumlem2  27455  dchrisum0lem1  27481  ostthlem2  27593  ostth2  27602  axlowdimlem3  28966  axlowdimlem6  28969  axlowdimlem7  28970  axlowdimlem16  28979  axlowdimlem17  28980  axlowdim  28983  clwwnrepclwwn  30368  fzspl  32818  fzdif2  32819  supfz  35872  divcnvlin  35876  nn0prpwlem  36465  fdc  37885  mettrifi  37897  caushft  37901  aks4d1lem1  42255  aks4d1p1  42269  aks4d1p2  42270  aks4d1p3  42271  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  aks4d1p9  42281  aks6d1c7lem1  42373  aks6d1c7lem2  42374  aks6d1c7  42377  aks5lem6  42385  aks5lem8  42394  aks5  42397  fzosumm1  42447  dffltz  42819  rmspecnonsq  43091  rmspecfund  43093  rmxyadd  43105  rmxy1  43106  jm2.18  43172  jm2.22  43179  jm2.15nn0  43187  jm2.16nn0  43188  jm2.27a  43189  jm2.27c  43191  jm3.1lem2  43202  jm3.1lem3  43203  jm3.1  43204  expdiophlem1  43205  dvgrat  44495  cvgdvgrat  44496  hashnzfz  44503  uzwo4  45240  ssinc  45273  ssdec  45274  rexanuz3  45282  monoords  45487  fzdifsuc2  45500  iuneqfzuzlem  45521  eluzelzd  45561  allbutfi  45579  eluzelz2  45589  uzid2  45591  monoordxrv  45667  monoord2xrv  45669  fmul01  45768  fmul01lt1lem1  45772  fmul01lt1lem2  45773  climsuselem1  45795  climsuse  45796  climf  45810  climresmpt  45845  climf2  45852  limsupequzlem  45908  limsupmnfuzlem  45912  limsupre3uzlem  45921  itgsinexp  46141  iblspltprt  46159  itgspltprt  46165  iundjiun  46646  smflimsuplem2  47007  smflimsuplem4  47009  smflimsuplem5  47010  fzopredsuc  47511  m1modmmod  47546  smonoord  47559  iccpartiltu  47610  fmtnoprmfac2lem1  47754  fmtnofac2lem  47756  lighneallem2  47794  lighneallem4a  47796  lighneallem4b  47797  fppr2odd  47919  fpprwpprb  47928  gboge9  47952  nnsum3primesle9  47982  nnsum4primesevenALTV  47989  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  bgoldbtbndlem2  47994  gpgusgralem  48244  gpgprismgr4cycllem9  48291  fllogbd  48748  fllog2  48756  dignn0ldlem  48790  dignnld  48791  digexp  48795  dignn0flhalf  48806  nn0sumshdiglemB  48808