Theorem eluzelz 12872

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6537   ≤ cle 11244  ℤcz 12591  ℤ_≥cuz 12862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-neg 11444  df-z 12592  df-uz 12863

This theorem is referenced by:  eluzelre  12873  uztrn  12880  uzneg  12882  uzss  12885  eluzp1l  12889  eluzadd  12891  eluzsub  12892  subeluzsub  12895  uzm1  12896  uzin  12898  uzind4  12930  uzwo  12935  uz2mulcl  12950  uzsupss  12964  elfz5  13544  elfzel2  13550  elfzelz  13552  eluzfz2  13560  peano2fzr  13565  fzsplit2  13577  fzopth  13589  ssfzunsn  13598  fzsuc  13599  elfz1uz  13622  uzsplit  13624  uzdisj  13625  fzm1  13635  uznfz  13638  nn0disj  13672  preduz  13678  elfzo3  13705  fzoss2  13716  fzouzsplit  13723  fzoun  13725  eluzgtdifelfzo  13756  fzosplitsnm1  13769  fzofzp1b  13794  elfzonelfzo  13798  fzosplitsn  13805  fzisfzounsn  13809  fldiv4lem1div2uz2  13869  m1modge3gt1  13954  modaddmodup  13970  om2uzlti  13986  om2uzf1oi  13989  uzrdgxfr  14003  fzen2  14005  seqfveq2  14060  seqfeq2  14061  seqshft2  14064  monoord  14068  monoord2  14069  sermono  14070  seqsplit  14071  seqf1olem1  14077  seqf1olem2  14078  seqid  14083  leexp2a  14208  expnlbnd2  14270  expmulnbnd  14271  hashfz  14464  fzsdom2  14465  hashfzo  14466  hashfzp1  14468  seqcoll  14501  swrdfv2  14699  pfxccatin12  14770  rexuz3  15400  r19.2uz  15403  rexuzre  15404  cau4  15408  caubnd2  15409  clim  15545  climrlim2  15598  climshft2  15633  climaddc1  15686  climmulc2  15688  climsubc1  15689  climsubc2  15690  clim2ser  15706  clim2ser2  15707  iserex  15708  climlec2  15710  climub  15713  isercolllem2  15717  isercoll  15719  isercoll2  15720  climcau  15722  caurcvg2  15729  caucvgb  15731  serf0  15732  iseraltlem1  15733  iseraltlem2  15734  iseralt  15736  sumrblem  15762  fsumcvg  15763  summolem2a  15766  fsumcvg2  15778  fsumm1  15802  fzosump1  15803  fsump1  15807  fsumrev2  15833  telfsumo  15854  fsumparts  15858  isumsplit  15894  isumrpcl  15897  isumsup2  15900  cvgrat  15937  mertenslem1  15938  clim2div  15943  prodeq2ii  15965  fprodcvg  15984  prodmolem2a  15988  zprod  15991  fprodntriv  15996  fprodser  16003  fprodm1  16021  fprodp1  16023  fprodeq0  16029  isprm3  16741  nprm  16746  dvdsprm  16762  exprmfct  16763  isprm5  16766  maxprmfct  16768  prmdvdsncoprmbd  16786  ncoprmlnprm  16787  phibndlem  16829  dfphi2  16833  hashdvds  16834  pcaddlem  16948  pcfac  16959  expnprm  16962  prmreclem4  16979  vdwlem8  17048  gsumval2a  18743  efgs1b  19806  telgsumfzs  20059  iscau4  25407  caucfil  25411  iscmet3lem3  25418  iscmet3lem1  25419  iscmet3lem2  25420  lmle  25429  uniioombllem3  25713  mbflimsup  25794  mbfi1fseqlem6  25848  dvfsumle  26149  dvfsumge  26150  dvfsumabs  26151  aaliou3lem1  26472  aaliou3lem2  26473  ulmres  26517  ulmshftlem  26518  ulmshft  26519  ulmcaulem  26523  ulmcau  26524  ulmdvlem1  26529  radcnvlem1  26542  logblt  26915  logbgcd1irr  26925  muval1  27263  chtdif  27288  ppidif  27293  chtub  27342  bcmono  27407  bpos1lem  27412  lgsquad2lem2  27515  2sqlem6  27553  2sqlem8a  27555  2sqlem8  27556  chebbnd1lem1  27599  dchrisumlem2  27620  dchrisum0lem1  27646  ostthlem2  27758  ostth2  27767  axlowdimlem3  29235  axlowdimlem6  29238  axlowdimlem7  29239  axlowdimlem16  29248  axlowdimlem17  29249  axlowdim  29252  clwwnrepclwwn  30636  fzspl  33075  fzdif2  33076  supfz  36154  divcnvlin  36158  nn0prpwlem  36756  fdc  38318  mettrifi  38330  caushft  38334  aks4d1lem1  42753  aks4d1p1  42767  aks4d1p2  42768  aks4d1p3  42769  aks4d1p5  42771  aks4d1p6  42772  aks4d1p7d1  42773  aks4d1p7  42774  aks4d1p8  42778  aks4d1p9  42779  aks6d1c7lem1  42871  aks6d1c7lem2  42872  aks6d1c7  42875  aks5lem6  42883  aks5lem8  42892  aks5  42895  fzosumm1  42942  dffltz  43292  rmspecnonsq  43560  rmspecfund  43562  rmxyadd  43574  rmxy1  43575  jm2.18  43641  jm2.22  43648  jm2.15nn0  43656  jm2.16nn0  43657  jm2.27a  43658  jm2.27c  43660  jm3.1lem2  43671  jm3.1lem3  43672  jm3.1  43673  expdiophlem1  43674  dvgrat  44948  cvgdvgrat  44949  hashnzfz  44956  uzwo4  45699  ssinc  45731  ssdec  45732  rexanuz3  45740  monoords  45942  fzdifsuc2  45955  iuneqfzuzlem  45976  eluzelzd  46016  allbutfi  46034  eluzelz2  46043  uzid2  46045  monoordxrv  46121  monoord2xrv  46123  fmul01  46222  fmul01lt1lem1  46226  fmul01lt1lem2  46227  climsuselem1  46249  climsuse  46250  climf  46264  climresmpt  46299  climf2  46306  limsupequzlem  46362  limsupmnfuzlem  46366  limsupre3uzlem  46375  itgsinexp  46595  iblspltprt  46613  itgspltprt  46619  iundjiun  47100  smflimsuplem2  47461  smflimsuplem4  47463  smflimsuplem5  47464  fzopredsuc  47984  m1modmmod  48024  smonoord  48037  2timesltsq  48038  2timesltsqm1  48039  iccpartiltu  48094  nprmmul1  48199  fmtnoprmfac2lem1  48241  fmtnofac2lem  48243  lighneallem2  48281  lighneallem4a  48283  lighneallem4b  48284  nprmdvdsfacm1lem1  48295  nprmdvdsfacm1lem4  48298  ppivalnnprm  48300  ppivalnnnprmge6  48301  ppivalnn  48307  fppr2odd  48419  fpprwpprb  48428  gboge9  48452  nnsum3primesle9  48482  nnsum4primesevenALTV  48489  wtgoldbnnsum4prm  48490  bgoldbnnsum3prm  48492  bgoldbtbndlem2  48494  gpgusgralem  48744  gpgprismgr4cycllem9  48791  fllogbd  49259  fllog2  49267  dignn0ldlem  49301  dignnld  49302  digexp  49306  dignn0flhalf  49317  nn0sumshdiglemB  49319