Theorem eluzelz 12241

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5030  ‘cfv 6324   ≤ cle 10665  ℤcz 11969  ℤ_≥cuz 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970  df-uz 12232

This theorem is referenced by:  eluzelre  12242  uztrn  12249  uzneg  12251  uzss  12253  eluzp1l  12257  eluzaddi  12259  eluzsubi  12260  subeluzsub  12263  uzm1  12264  uzin  12266  uzind4  12294  uzwo  12299  uz2mulcl  12314  uzsupss  12328  elfz5  12894  elfzel2  12900  elfzelz  12902  eluzfz2  12910  peano2fzr  12915  fzsplit2  12927  fzopth  12939  ssfzunsn  12948  fzsuc  12949  elfz1uz  12972  uzsplit  12974  uzdisj  12975  fzm1  12982  uznfz  12985  nn0disj  13018  preduz  13024  elfzo3  13049  fzoss2  13060  fzouzsplit  13067  fzoun  13069  eluzgtdifelfzo  13094  fzosplitsnm1  13107  fzofzp1b  13130  elfzonelfzo  13134  fzosplitsn  13140  fzisfzounsn  13144  fldiv4lem1div2uz2  13201  m1modge3gt1  13281  modaddmodup  13297  om2uzlti  13313  om2uzf1oi  13316  uzrdgxfr  13330  fzen2  13332  seqfveq2  13388  seqfeq2  13389  seqshft2  13392  monoord  13396  monoord2  13397  sermono  13398  seqsplit  13399  seqf1olem1  13405  seqf1olem2  13406  seqid  13411  seqz  13414  leexp2a  13532  expnlbnd2  13591  expmulnbnd  13592  hashfz  13784  fzsdom2  13785  hashfzo  13786  hashfzp1  13788  seqcoll  13818  swrdfv2  14014  pfxccatin12  14086  rexuz3  14700  r19.2uz  14703  rexuzre  14704  cau4  14708  caubnd2  14709  clim  14843  climrlim2  14896  climshft2  14931  climaddc1  14983  climmulc2  14985  climsubc1  14986  climsubc2  14987  clim2ser  15003  clim2ser2  15004  iserex  15005  climlec2  15007  climub  15010  isercolllem2  15014  isercoll  15016  isercoll2  15017  climcau  15019  caurcvg2  15026  caucvgb  15028  serf0  15029  iseraltlem1  15030  iseraltlem2  15031  iseralt  15033  sumrblem  15060  fsumcvg  15061  summolem2a  15064  fsumcvg2  15076  fsumm1  15098  fzosump1  15099  fsump1  15103  fsumrev2  15129  telfsumo  15149  fsumparts  15153  isumsplit  15187  isumrpcl  15190  isumsup2  15193  cvgrat  15231  mertenslem1  15232  clim2div  15237  prodeq2ii  15259  fprodcvg  15276  prodmolem2a  15280  zprod  15283  fprodntriv  15288  fprodser  15295  fprodm1  15313  fprodp1  15315  fprodeq0  15321  isprm3  16017  nprm  16022  dvdsprm  16037  exprmfct  16038  isprm5  16041  maxprmfct  16043  ncoprmlnprm  16058  phibndlem  16097  dfphi2  16101  hashdvds  16102  pcaddlem  16214  pcfac  16225  expnprm  16228  prmreclem4  16245  vdwlem8  16314  gsumval2a  17887  efgs1b  18854  telgsumfzs  19102  iscau4  23883  caucfil  23887  iscmet3lem3  23894  iscmet3lem1  23895  iscmet3lem2  23896  lmle  23905  uniioombllem3  24189  mbflimsup  24270  mbfi1fseqlem6  24324  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  aaliou3lem1  24938  aaliou3lem2  24939  ulmres  24983  ulmshftlem  24984  ulmshft  24985  ulmcaulem  24989  ulmcau  24990  ulmdvlem1  24995  radcnvlem1  25008  logblt  25370  logbgcd1irr  25380  muval1  25718  chtdif  25743  ppidif  25748  chtub  25796  bcmono  25861  bpos1lem  25866  lgsquad2lem2  25969  2sqlem6  26007  2sqlem8a  26009  2sqlem8  26010  chebbnd1lem1  26053  dchrisumlem2  26074  dchrisum0lem1  26100  ostthlem2  26212  ostth2  26221  axlowdimlem3  26738  axlowdimlem6  26741  axlowdimlem7  26742  axlowdimlem16  26751  axlowdimlem17  26752  axlowdim  26755  clwwnrepclwwn  28129  fzspl  30539  fzdif2  30540  supfz  33073  divcnvlin  33077  nn0prpwlem  33783  fdc  35183  mettrifi  35195  caushft  35199  fzosumm1  39421  dffltz  39615  fltne  39616  rmspecnonsq  39848  rmspecfund  39850  rmxyadd  39862  rmxy1  39863  jm2.18  39929  jm2.22  39936  jm2.15nn0  39944  jm2.16nn0  39945  jm2.27a  39946  jm2.27c  39948  jm3.1lem2  39959  jm3.1lem3  39960  jm3.1  39961  expdiophlem1  39962  dvgrat  41016  cvgdvgrat  41017  hashnzfz  41024  uzwo4  41687  ssinc  41723  ssdec  41724  rexanuz3  41732  monoords  41929  fzdifsuc2  41942  iuneqfzuzlem  41966  eluzelzd  42007  allbutfi  42029  eluzelz2  42040  uzid2  42042  monoordxrv  42121  monoord2xrv  42123  fmul01  42222  fmul01lt1lem1  42226  fmul01lt1lem2  42227  climsuselem1  42249  climsuse  42250  climf  42264  climresmpt  42301  climf2  42308  limsupequzlem  42364  limsupmnfuzlem  42368  limsupre3uzlem  42377  itgsinexp  42597  iblspltprt  42615  itgspltprt  42621  iundjiun  43099  smflimsuplem2  43452  smflimsuplem4  43454  smflimsuplem5  43455  fzopredsuc  43880  smonoord  43888  iccpartiltu  43939  fmtnoprmfac2lem1  44083  fmtnofac2lem  44085  lighneallem2  44124  lighneallem4a  44126  lighneallem4b  44127  fppr2odd  44249  fpprwpprb  44258  gboge9  44282  nnsum3primesle9  44312  nnsum4primesevenALTV  44319  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbndlem2  44324  m1modmmod  44935  fllogbd  44974  fllog2  44982  dignn0ldlem  45016  dignnld  45017  digexp  45021  dignn0flhalf  45032  nn0sumshdiglemB  45034