Theorem eluzelz 12745

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  ‘cfv 6482   ≤ cle 11150  ℤcz 12471  ℤ_≥cuz 12735

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  eluzelre  12746  uztrn  12753  uzneg  12755  uzss  12758  eluzp1l  12762  eluzadd  12764  eluzsub  12765  eluzaddiOLD  12767  eluzsubiOLD  12769  subeluzsub  12772  uzm1  12773  uzin  12775  uzind4  12807  uzwo  12812  uz2mulcl  12827  uzsupss  12841  elfz5  13419  elfzel2  13425  elfzelz  13427  eluzfz2  13435  peano2fzr  13440  fzsplit2  13452  fzopth  13464  ssfzunsn  13473  fzsuc  13474  elfz1uz  13497  uzsplit  13499  uzdisj  13500  fzm1  13510  uznfz  13513  nn0disj  13547  preduz  13553  elfzo3  13579  fzoss2  13590  fzouzsplit  13597  fzoun  13599  eluzgtdifelfzo  13630  fzosplitsnm1  13643  fzofzp1b  13668  elfzonelfzo  13672  fzosplitsn  13678  fzisfzounsn  13682  fldiv4lem1div2uz2  13740  m1modge3gt1  13825  modaddmodup  13841  om2uzlti  13857  om2uzf1oi  13860  uzrdgxfr  13874  fzen2  13876  seqfveq2  13931  seqfeq2  13932  seqshft2  13935  monoord  13939  monoord2  13940  sermono  13941  seqsplit  13942  seqf1olem1  13948  seqf1olem2  13949  seqid  13954  leexp2a  14079  expnlbnd2  14141  expmulnbnd  14142  hashfz  14334  fzsdom2  14335  hashfzo  14336  hashfzp1  14338  seqcoll  14371  swrdfv2  14568  pfxccatin12  14639  rexuz3  15256  r19.2uz  15259  rexuzre  15260  cau4  15264  caubnd2  15265  clim  15401  climrlim2  15454  climshft2  15489  climaddc1  15542  climmulc2  15544  climsubc1  15545  climsubc2  15546  clim2ser  15562  clim2ser2  15563  iserex  15564  climlec2  15566  climub  15569  isercolllem2  15573  isercoll  15575  isercoll2  15576  climcau  15578  caurcvg2  15585  caucvgb  15587  serf0  15588  iseraltlem1  15589  iseraltlem2  15590  iseralt  15592  sumrblem  15618  fsumcvg  15619  summolem2a  15622  fsumcvg2  15634  fsumm1  15658  fzosump1  15659  fsump1  15663  fsumrev2  15689  telfsumo  15709  fsumparts  15713  isumsplit  15747  isumrpcl  15750  isumsup2  15753  cvgrat  15790  mertenslem1  15791  clim2div  15796  prodeq2ii  15818  fprodcvg  15837  prodmolem2a  15841  zprod  15844  fprodntriv  15849  fprodser  15856  fprodm1  15874  fprodp1  15876  fprodeq0  15882  isprm3  16594  nprm  16599  dvdsprm  16614  exprmfct  16615  isprm5  16618  maxprmfct  16620  prmdvdsncoprmbd  16638  ncoprmlnprm  16639  phibndlem  16681  dfphi2  16685  hashdvds  16686  pcaddlem  16800  pcfac  16811  expnprm  16814  prmreclem4  16831  vdwlem8  16900  gsumval2a  18559  efgs1b  19615  telgsumfzs  19868  iscau4  25177  caucfil  25181  iscmet3lem3  25188  iscmet3lem1  25189  iscmet3lem2  25190  lmle  25199  uniioombllem3  25484  mbflimsup  25565  mbfi1fseqlem6  25619  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumabs  25927  aaliou3lem1  26248  aaliou3lem2  26249  ulmres  26295  ulmshftlem  26296  ulmshft  26297  ulmcaulem  26301  ulmcau  26302  ulmdvlem1  26307  radcnvlem1  26320  logblt  26692  logbgcd1irr  26702  muval1  27041  chtdif  27066  ppidif  27071  chtub  27121  bcmono  27186  bpos1lem  27191  lgsquad2lem2  27294  2sqlem6  27332  2sqlem8a  27334  2sqlem8  27335  chebbnd1lem1  27378  dchrisumlem2  27399  dchrisum0lem1  27425  ostthlem2  27537  ostth2  27546  axlowdimlem3  28889  axlowdimlem6  28892  axlowdimlem7  28893  axlowdimlem16  28902  axlowdimlem17  28903  axlowdim  28906  clwwnrepclwwn  30288  fzspl  32733  fzdif2  32734  supfz  35712  divcnvlin  35716  nn0prpwlem  36306  fdc  37735  mettrifi  37747  caushft  37751  aks4d1lem1  42045  aks4d1p1  42059  aks4d1p2  42060  aks4d1p3  42061  aks4d1p5  42063  aks4d1p6  42064  aks4d1p7d1  42065  aks4d1p7  42066  aks4d1p8  42070  aks4d1p9  42071  aks6d1c7lem1  42163  aks6d1c7lem2  42164  aks6d1c7  42167  aks5lem6  42175  aks5lem8  42184  aks5  42187  fzosumm1  42233  dffltz  42617  rmspecnonsq  42890  rmspecfund  42892  rmxyadd  42904  rmxy1  42905  jm2.18  42971  jm2.22  42978  jm2.15nn0  42986  jm2.16nn0  42987  jm2.27a  42988  jm2.27c  42990  jm3.1lem2  43001  jm3.1lem3  43002  jm3.1  43003  expdiophlem1  43004  dvgrat  44295  cvgdvgrat  44296  hashnzfz  44303  uzwo4  45041  ssinc  45075  ssdec  45076  rexanuz3  45084  monoords  45289  fzdifsuc2  45302  iuneqfzuzlem  45324  eluzelzd  45364  allbutfi  45382  eluzelz2  45392  uzid2  45394  monoordxrv  45470  monoord2xrv  45472  fmul01  45571  fmul01lt1lem1  45575  fmul01lt1lem2  45576  climsuselem1  45598  climsuse  45599  climf  45613  climresmpt  45650  climf2  45657  limsupequzlem  45713  limsupmnfuzlem  45717  limsupre3uzlem  45726  itgsinexp  45946  iblspltprt  45964  itgspltprt  45970  iundjiun  46451  smflimsuplem2  46812  smflimsuplem4  46814  smflimsuplem5  46815  fzopredsuc  47317  m1modmmod  47352  smonoord  47365  iccpartiltu  47416  fmtnoprmfac2lem1  47560  fmtnofac2lem  47562  lighneallem2  47600  lighneallem4a  47602  lighneallem4b  47603  fppr2odd  47725  fpprwpprb  47734  gboge9  47758  nnsum3primesle9  47788  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem2  47800  gpgusgralem  48050  gpgprismgr4cycllem9  48097  fllogbd  48555  fllog2  48563  dignn0ldlem  48597  dignnld  48598  digexp  48602  dignn0flhalf  48613  nn0sumshdiglemB  48615