Theorem eluzelz 11978

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

Syntax hints:   → wi 4   ∈ wcel 2166   class class class wbr 4873  ‘cfv 6123   ≤ cle 10392  ℤcz 11704  ℤ_≥cuz 11968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-cnex 10308  ax-resscn 10309

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131  df-ov 6908  df-neg 10588  df-z 11705  df-uz 11969

This theorem is referenced by:  eluzelre  11979  uztrn  11985  uzneg  11987  uzss  11989  eluzp1l  11993  eluzaddi  11995  eluzsubi  11996  subeluzsub  11999  uzm1  12000  uzin  12002  uzind4  12028  uzwo  12034  uz2mulcl  12049  uzsupss  12063  elfz5  12627  elfzel2  12633  elfzelz  12635  eluzfz2  12642  peano2fzr  12647  fzsplit2  12659  fzopth  12671  ssfzunsn  12680  fzsuc  12681  elfz1uz  12704  uzsplit  12706  uzdisj  12707  fzm1  12714  uznfz  12717  nn0disj  12750  preduz  12756  elfzo3  12781  fzoss2  12791  fzouzsplit  12798  fzoun  12800  eluzgtdifelfzo  12825  fzosplitsnm1  12838  fzofzp1b  12861  elfzonelfzo  12865  fzosplitsn  12871  fzisfzounsn  12875  fldiv4lem1div2uz2  12932  m1modge3gt1  13012  modaddmodup  13028  om2uzlti  13044  om2uzf1oi  13047  uzrdgxfr  13061  fzen2  13063  seqfveq2  13117  seqfeq2  13118  seqshft2  13121  monoord  13125  monoord2  13126  sermono  13127  seqsplit  13128  seqf1olem1  13134  seqf1olem2  13135  seqid  13140  seqz  13143  leexp2a  13210  expnlbnd2  13289  expmulnbnd  13290  hashfz  13503  fzsdom2  13504  hashfzo  13505  hashfzp1  13507  seqcoll  13537  swrdfv2  13735  pfxccatin12  13831  swrdccatin12OLD  13832  rexuz3  14465  r19.2uz  14468  rexuzre  14469  cau4  14473  caubnd2  14474  clim  14602  climrlim2  14655  climshft2  14690  climaddc1  14742  climmulc2  14744  climsubc1  14745  climsubc2  14746  clim2ser  14762  clim2ser2  14763  iserex  14764  climlec2  14766  climub  14769  isercolllem2  14773  isercoll  14775  isercoll2  14776  climcau  14778  caurcvg2  14785  caucvgb  14787  serf0  14788  iseraltlem1  14789  iseraltlem2  14790  iseralt  14792  sumrblem  14819  fsumcvg  14820  summolem2a  14823  fsumcvg2  14835  fsumm1  14857  fzosump1  14858  fsump1  14862  fsumrev2  14888  telfsumo  14908  fsumparts  14912  isumsplit  14946  isumrpcl  14949  isumsup2  14952  cvgrat  14988  mertenslem1  14989  clim2div  14994  prodeq2ii  15016  fprodcvg  15033  prodmolem2a  15037  zprod  15040  fprodntriv  15045  fprodser  15052  fprodm1  15070  fprodp1  15072  fprodeq0  15078  isprm3  15768  nprm  15773  dvdsprm  15786  exprmfct  15787  isprm5  15790  maxprmfct  15792  ncoprmlnprm  15807  phibndlem  15846  dfphi2  15850  hashdvds  15851  pcaddlem  15963  pcfac  15974  expnprm  15977  prmreclem4  15994  vdwlem8  16063  gsumval2a  17632  efgs1b  18500  telgsumfzs  18740  iscau4  23447  caucfil  23451  iscmet3lem3  23458  iscmet3lem1  23459  iscmet3lem2  23460  lmle  23469  uniioombllem3  23751  mbflimsup  23832  mbfi1fseqlem6  23886  dvfsumle  24183  dvfsumge  24184  dvfsumabs  24185  aaliou3lem1  24496  aaliou3lem2  24497  ulmres  24541  ulmshftlem  24542  ulmshft  24543  ulmcaulem  24547  ulmcau  24548  ulmdvlem1  24553  radcnvlem1  24566  logblt  24924  logbgcd1irr  24934  muval1  25272  chtdif  25297  ppidif  25302  chtub  25350  bcmono  25415  bpos1lem  25420  lgsquad2lem2  25523  2sqlem6  25561  2sqlem8a  25563  2sqlem8  25564  chebbnd1lem1  25571  dchrisumlem2  25592  dchrisum0lem1  25618  ostthlem2  25730  ostth2  25739  axlowdimlem3  26243  axlowdimlem6  26246  axlowdimlem7  26247  axlowdimlem16  26256  axlowdimlem17  26257  axlowdim  26260  clwwnrepclwwn  27726  clwwnrepclwwnOLD  27727  fzspl  30097  fzdif2  30098  supfz  32156  divcnvlin  32160  nn0prpwlem  32855  fdc  34083  mettrifi  34095  caushft  34099  dffltz  38097  rmspecnonsq  38315  rmspecfund  38317  rmxyadd  38329  rmxy1  38330  jm2.18  38398  jm2.22  38405  jm2.15nn0  38413  jm2.16nn0  38414  jm2.27a  38415  jm2.27c  38417  jm3.1lem2  38428  jm3.1lem3  38429  jm3.1  38430  expdiophlem1  38431  dvgrat  39351  cvgdvgrat  39352  hashnzfz  39359  uzwo4  40038  ssinc  40081  ssdec  40082  rexanuz3  40092  monoords  40309  fzdifsuc2  40322  iuneqfzuzlem  40347  eluzelzd  40388  allbutfi  40411  eluzelz2  40422  uzid2  40425  monoordxrv  40506  monoord2xrv  40508  fmul01  40607  fmul01lt1lem1  40611  fmul01lt1lem2  40612  climsuselem1  40634  climsuse  40635  climf  40649  climresmpt  40686  climf2  40693  limsupequzlem  40749  limsupmnfuzlem  40753  limsupre3uzlem  40762  itgsinexp  40965  iblspltprt  40983  itgspltprt  40989  iundjiunlem  41467  iundjiun  41468  smflimsuplem2  41821  smflimsuplem4  41823  smflimsuplem5  41824  fzopredsuc  42221  smonoord  42229  iccpartiltu  42246  fmtnoprmfac2lem1  42308  fmtnofac2lem  42310  lighneallem2  42353  lighneallem4a  42355  lighneallem4b  42356  gboge9  42482  nnsum3primesle9  42512  nnsum4primesevenALTV  42519  wtgoldbnnsum4prm  42520  bgoldbnnsum3prm  42522  bgoldbtbndlem2  42524  m1modmmod  43163  fllogbd  43201  fllog2  43209  dignn0ldlem  43243  dignnld  43244  digexp  43248  dignn0flhalf  43259  nn0sumshdiglemB  43261