Theorem eluzelz 12810

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5110  ‘cfv 6514   ≤ cle 11216  ℤcz 12536  ℤ_≥cuz 12800

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-cnex 11131  ax-resscn 11132

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537  df-uz 12801

This theorem is referenced by:  eluzelre  12811  uztrn  12818  uzneg  12820  uzss  12823  eluzp1l  12827  eluzadd  12829  eluzsub  12830  eluzaddiOLD  12832  eluzsubiOLD  12834  subeluzsub  12837  uzm1  12838  uzin  12840  uzind4  12872  uzwo  12877  uz2mulcl  12892  uzsupss  12906  elfz5  13484  elfzel2  13490  elfzelz  13492  eluzfz2  13500  peano2fzr  13505  fzsplit2  13517  fzopth  13529  ssfzunsn  13538  fzsuc  13539  elfz1uz  13562  uzsplit  13564  uzdisj  13565  fzm1  13575  uznfz  13578  nn0disj  13612  preduz  13618  elfzo3  13644  fzoss2  13655  fzouzsplit  13662  fzoun  13664  eluzgtdifelfzo  13695  fzosplitsnm1  13708  fzofzp1b  13733  elfzonelfzo  13737  fzosplitsn  13743  fzisfzounsn  13747  fldiv4lem1div2uz2  13805  m1modge3gt1  13890  modaddmodup  13906  om2uzlti  13922  om2uzf1oi  13925  uzrdgxfr  13939  fzen2  13941  seqfveq2  13996  seqfeq2  13997  seqshft2  14000  monoord  14004  monoord2  14005  sermono  14006  seqsplit  14007  seqf1olem1  14013  seqf1olem2  14014  seqid  14019  leexp2a  14144  expnlbnd2  14206  expmulnbnd  14207  hashfz  14399  fzsdom2  14400  hashfzo  14401  hashfzp1  14403  seqcoll  14436  swrdfv2  14633  pfxccatin12  14705  rexuz3  15322  r19.2uz  15325  rexuzre  15326  cau4  15330  caubnd2  15331  clim  15467  climrlim2  15520  climshft2  15555  climaddc1  15608  climmulc2  15610  climsubc1  15611  climsubc2  15612  clim2ser  15628  clim2ser2  15629  iserex  15630  climlec2  15632  climub  15635  isercolllem2  15639  isercoll  15641  isercoll2  15642  climcau  15644  caurcvg2  15651  caucvgb  15653  serf0  15654  iseraltlem1  15655  iseraltlem2  15656  iseralt  15658  sumrblem  15684  fsumcvg  15685  summolem2a  15688  fsumcvg2  15700  fsumm1  15724  fzosump1  15725  fsump1  15729  fsumrev2  15755  telfsumo  15775  fsumparts  15779  isumsplit  15813  isumrpcl  15816  isumsup2  15819  cvgrat  15856  mertenslem1  15857  clim2div  15862  prodeq2ii  15884  fprodcvg  15903  prodmolem2a  15907  zprod  15910  fprodntriv  15915  fprodser  15922  fprodm1  15940  fprodp1  15942  fprodeq0  15948  isprm3  16660  nprm  16665  dvdsprm  16680  exprmfct  16681  isprm5  16684  maxprmfct  16686  prmdvdsncoprmbd  16704  ncoprmlnprm  16705  phibndlem  16747  dfphi2  16751  hashdvds  16752  pcaddlem  16866  pcfac  16877  expnprm  16880  prmreclem4  16897  vdwlem8  16966  gsumval2a  18619  efgs1b  19673  telgsumfzs  19926  iscau4  25186  caucfil  25190  iscmet3lem3  25197  iscmet3lem1  25198  iscmet3lem2  25199  lmle  25208  uniioombllem3  25493  mbflimsup  25574  mbfi1fseqlem6  25628  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  aaliou3lem1  26257  aaliou3lem2  26258  ulmres  26304  ulmshftlem  26305  ulmshft  26306  ulmcaulem  26310  ulmcau  26311  ulmdvlem1  26316  radcnvlem1  26329  logblt  26701  logbgcd1irr  26711  muval1  27050  chtdif  27075  ppidif  27080  chtub  27130  bcmono  27195  bpos1lem  27200  lgsquad2lem2  27303  2sqlem6  27341  2sqlem8a  27343  2sqlem8  27344  chebbnd1lem1  27387  dchrisumlem2  27408  dchrisum0lem1  27434  ostthlem2  27546  ostth2  27555  axlowdimlem3  28878  axlowdimlem6  28881  axlowdimlem7  28882  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  clwwnrepclwwn  30280  fzspl  32719  fzdif2  32720  supfz  35723  divcnvlin  35727  nn0prpwlem  36317  fdc  37746  mettrifi  37758  caushft  37762  aks4d1lem1  42057  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  aks6d1c7lem1  42175  aks6d1c7lem2  42176  aks6d1c7  42179  aks5lem6  42187  aks5lem8  42196  aks5  42199  fzosumm1  42245  dffltz  42629  rmspecnonsq  42902  rmspecfund  42904  rmxyadd  42917  rmxy1  42918  jm2.18  42984  jm2.22  42991  jm2.15nn0  42999  jm2.16nn0  43000  jm2.27a  43001  jm2.27c  43003  jm3.1lem2  43014  jm3.1lem3  43015  jm3.1  43016  expdiophlem1  43017  dvgrat  44308  cvgdvgrat  44309  hashnzfz  44316  uzwo4  45054  ssinc  45088  ssdec  45089  rexanuz3  45097  monoords  45302  fzdifsuc2  45315  iuneqfzuzlem  45337  eluzelzd  45378  allbutfi  45396  eluzelz2  45406  uzid2  45408  monoordxrv  45484  monoord2xrv  45486  fmul01  45585  fmul01lt1lem1  45589  fmul01lt1lem2  45590  climsuselem1  45612  climsuse  45613  climf  45627  climresmpt  45664  climf2  45671  limsupequzlem  45727  limsupmnfuzlem  45731  limsupre3uzlem  45740  itgsinexp  45960  iblspltprt  45978  itgspltprt  45984  iundjiun  46465  smflimsuplem2  46826  smflimsuplem4  46828  smflimsuplem5  46829  fzopredsuc  47328  m1modmmod  47363  smonoord  47376  iccpartiltu  47427  fmtnoprmfac2lem1  47571  fmtnofac2lem  47573  lighneallem2  47611  lighneallem4a  47613  lighneallem4b  47614  fppr2odd  47736  fpprwpprb  47745  gboge9  47769  nnsum3primesle9  47799  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem2  47811  gpgusgralem  48051  gpgprismgr4cycllem9  48097  fllogbd  48553  fllog2  48561  dignn0ldlem  48595  dignnld  48596  digexp  48600  dignn0flhalf  48611  nn0sumshdiglemB  48613