Theorem eluzelz 12849

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  ‘cfv 6521   ≤ cle 11217  ℤcz 12568  ℤ_≥cuz 12839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569  df-uz 12840

This theorem is referenced by:  eluzelre  12850  uztrn  12857  uzneg  12859  uzss  12862  eluzp1l  12866  eluzadd  12868  eluzsub  12869  subeluzsub  12872  uzm1  12873  uzin  12875  uzind4  12907  uzwo  12912  uz2mulcl  12927  uzsupss  12941  elfz5  13521  elfzel2  13527  elfzelz  13529  eluzfz2  13537  peano2fzr  13542  fzsplit2  13554  fzopth  13566  ssfzunsn  13575  fzsuc  13576  elfz1uz  13599  uzsplit  13601  uzdisj  13602  fzm1  13612  uznfz  13615  nn0disj  13649  preduz  13655  elfzo3  13682  fzoss2  13693  fzouzsplit  13700  fzoun  13702  eluzgtdifelfzo  13733  fzosplitsnm1  13746  fzofzp1b  13771  elfzonelfzo  13775  fzosplitsn  13782  fzisfzounsn  13786  fldiv4lem1div2uz2  13846  m1modge3gt1  13931  modaddmodup  13947  om2uzlti  13963  om2uzf1oi  13966  uzrdgxfr  13980  fzen2  13982  seqfveq2  14037  seqfeq2  14038  seqshft2  14041  monoord  14045  monoord2  14046  sermono  14047  seqsplit  14048  seqf1olem1  14054  seqf1olem2  14055  seqid  14060  leexp2a  14185  expnlbnd2  14247  expmulnbnd  14248  hashfz  14440  fzsdom2  14441  hashfzo  14442  hashfzp1  14444  seqcoll  14477  swrdfv2  14675  pfxccatin12  14746  rexuz3  15376  r19.2uz  15379  rexuzre  15380  cau4  15384  caubnd2  15385  clim  15521  climrlim2  15574  climshft2  15609  climaddc1  15662  climmulc2  15664  climsubc1  15665  climsubc2  15666  clim2ser  15682  clim2ser2  15683  iserex  15684  climlec2  15686  climub  15689  isercolllem2  15693  isercoll  15695  isercoll2  15696  climcau  15698  caurcvg2  15705  caucvgb  15707  serf0  15708  iseraltlem1  15709  iseraltlem2  15710  iseralt  15712  sumrblem  15738  fsumcvg  15739  summolem2a  15742  fsumcvg2  15754  fsumm1  15778  fzosump1  15779  fsump1  15783  fsumrev2  15809  telfsumo  15830  fsumparts  15834  isumsplit  15870  isumrpcl  15873  isumsup2  15876  cvgrat  15913  mertenslem1  15914  clim2div  15919  prodeq2ii  15941  fprodcvg  15960  prodmolem2a  15964  zprod  15967  fprodntriv  15972  fprodser  15979  fprodm1  15997  fprodp1  15999  fprodeq0  16005  isprm3  16717  nprm  16722  dvdsprm  16738  exprmfct  16739  isprm5  16742  maxprmfct  16744  prmdvdsncoprmbd  16762  ncoprmlnprm  16763  phibndlem  16805  dfphi2  16809  hashdvds  16810  pcaddlem  16924  pcfac  16935  expnprm  16938  prmreclem4  16955  vdwlem8  17024  gsumval2a  18719  efgs1b  19776  telgsumfzs  20029  iscau4  25341  caucfil  25345  iscmet3lem3  25352  iscmet3lem1  25353  iscmet3lem2  25354  lmle  25363  uniioombllem3  25647  mbflimsup  25728  mbfi1fseqlem6  25782  dvfsumle  26083  dvfsumge  26084  dvfsumabs  26085  aaliou3lem1  26406  aaliou3lem2  26407  ulmres  26451  ulmshftlem  26452  ulmshft  26453  ulmcaulem  26457  ulmcau  26458  ulmdvlem1  26463  radcnvlem1  26476  logblt  26849  logbgcd1irr  26859  muval1  27197  chtdif  27222  ppidif  27227  chtub  27276  bcmono  27341  bpos1lem  27346  lgsquad2lem2  27449  2sqlem6  27487  2sqlem8a  27489  2sqlem8  27490  chebbnd1lem1  27533  dchrisumlem2  27554  dchrisum0lem1  27580  ostthlem2  27692  ostth2  27701  axlowdimlem3  29145  axlowdimlem6  29148  axlowdimlem7  29149  axlowdimlem16  29158  axlowdimlem17  29159  axlowdim  29162  clwwnrepclwwn  30546  fzspl  32991  fzdif2  32992  supfz  36079  divcnvlin  36083  nn0prpwlem  36682  fdc  38244  mettrifi  38256  caushft  38260  aks4d1lem1  42679  aks4d1p1  42693  aks4d1p2  42694  aks4d1p3  42695  aks4d1p5  42697  aks4d1p6  42698  aks4d1p7d1  42699  aks4d1p7  42700  aks4d1p8  42704  aks4d1p9  42705  aks6d1c7lem1  42797  aks6d1c7lem2  42798  aks6d1c7  42801  aks5lem6  42809  aks5lem8  42818  aks5  42821  fzosumm1  42866  dffltz  43216  rmspecnonsq  43484  rmspecfund  43486  rmxyadd  43498  rmxy1  43499  jm2.18  43565  jm2.22  43572  jm2.15nn0  43580  jm2.16nn0  43581  jm2.27a  43582  jm2.27c  43584  jm3.1lem2  43595  jm3.1lem3  43596  jm3.1  43597  expdiophlem1  43598  dvgrat  44888  cvgdvgrat  44889  hashnzfz  44896  uzwo4  45633  ssinc  45665  ssdec  45666  rexanuz3  45674  monoords  45876  fzdifsuc2  45889  iuneqfzuzlem  45910  eluzelzd  45950  allbutfi  45968  eluzelz2  45977  uzid2  45979  monoordxrv  46055  monoord2xrv  46057  fmul01  46156  fmul01lt1lem1  46160  fmul01lt1lem2  46161  climsuselem1  46183  climsuse  46184  climf  46198  climresmpt  46233  climf2  46240  limsupequzlem  46296  limsupmnfuzlem  46300  limsupre3uzlem  46309  itgsinexp  46529  iblspltprt  46547  itgspltprt  46553  iundjiun  47034  smflimsuplem2  47395  smflimsuplem4  47397  smflimsuplem5  47398  fzopredsuc  47918  m1modmmod  47958  smonoord  47971  2timesltsq  47972  2timesltsqm1  47973  iccpartiltu  48028  nprmmul1  48133  fmtnoprmfac2lem1  48175  fmtnofac2lem  48177  lighneallem2  48215  lighneallem4a  48217  lighneallem4b  48218  nprmdvdsfacm1lem1  48229  nprmdvdsfacm1lem4  48232  ppivalnnprm  48234  ppivalnnnprmge6  48235  ppivalnn  48241  fppr2odd  48353  fpprwpprb  48362  gboge9  48386  nnsum3primesle9  48416  nnsum4primesevenALTV  48423  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  bgoldbtbndlem2  48428  gpgusgralem  48678  gpgprismgr4cycllem9  48725  fllogbd  49182  fllog2  49190  dignn0ldlem  49224  dignnld  49225  digexp  49229  dignn0flhalf  49240  nn0sumshdiglemB  49242