Theorem eluzelz 9727

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

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4082  ‘cfv 5317   ≤ cle 8178  ℤcz 9442  ℤ_≥cuz 9718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-cnex 8086  ax-resscn 8087

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-ima 4731  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-fv 5325  df-ov 6003  df-neg 8316  df-z 9443  df-uz 9719

This theorem is referenced by:  eluzelre  9728  uztrn  9735  uzneg  9737  uzssz  9738  uzss  9739  eluzp1l  9743  eluzaddi  9745  eluzsubi  9746  eluzadd  9747  eluzsub  9748  uzm1  9749  uzin  9751  uzind4  9779  uz2mulcl  9799  elfz5  10209  elfzel2  10215  elfzelz  10217  eluzfz2  10224  peano2fzr  10229  fzsplit2  10242  fzopth  10253  fzsuc  10261  elfzp1  10264  fzdifsuc  10273  uzsplit  10284  uzdisj  10285  fzm1  10292  fzneuz  10293  uznfz  10295  nn0disj  10330  elfzo3  10356  fzoss2  10366  fzouzsplit  10373  fzoun  10375  eluzgtdifelfzo  10398  fzosplitsnm1  10410  fzofzp1b  10429  elfzonelfzo  10431  fzosplitsn  10434  fzisfzounsn  10437  zsupcllemstep  10444  infssuzex  10448  suprzubdc  10451  fldiv4lem1div2uz2  10521  mulp1mod1  10582  m1modge3gt1  10588  frec2uzltd  10620  frecfzen2  10644  uzennn  10653  uzsinds  10661  seq3fveq2  10692  seq3feq2  10693  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord  10702  monoord2  10703  ser3mono  10704  seq3split  10705  seqsplitg  10706  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  seq3f1olemqsumk  10729  seq3f1olemp  10732  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  seq3id  10742  seq3z  10745  fser0const  10752  leexp2a  10809  expnlbnd2  10882  hashfz  11038  hashfzo  11039  hashfzp1  11041  seq3coll  11059  swrdfv2  11190  pfxccatin12  11260  seq3shft  11344  rexuz3  11496  r19.2uz  11499  cau4  11622  caubnd2  11623  clim  11787  climshft2  11812  climaddc1  11835  climmulc2  11837  climsubc1  11838  climsubc2  11839  clim2ser  11843  clim2ser2  11844  iserex  11845  climlec2  11847  climub  11850  climcau  11853  climcaucn  11857  serf0  11858  sumrbdclem  11883  fsum3cvg  11884  summodclem2a  11887  zsumdc  11890  fsum3  11893  fisumss  11898  fsum3cvg2  11900  fsum3ser  11903  fsumcl2lem  11904  fsumadd  11912  fsumm1  11922  fzosump1  11923  fsum1p  11924  fsump1  11926  fsummulc2  11954  telfsumo  11972  fsumparts  11976  iserabs  11981  binomlem  11989  isumshft  11996  isumsplit  11997  isumrpcl  12000  divcnv  12003  trireciplem  12006  geosergap  12012  geolim2  12018  cvgratnnlemseq  12032  cvgratnnlemabsle  12033  cvgratnnlemsumlt  12034  cvgratnnlemrate  12036  cvgratz  12038  cvgratgt0  12039  mertenslemi1  12041  clim2divap  12046  prodrbdclem  12077  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodntrivap  12090  fprodssdc  12096  fprodm1  12104  fprod1p  12105  fprodp1  12106  fprodabs  12122  fprodeq0  12123  efgt1p2  12201  modm1div  12306  dvdsbnd  12472  uzwodc  12553  ncoprmgcdne1b  12606  isprm3  12635  prmind2  12637  nprm  12640  dvdsprm  12654  exprmfct  12655  isprm5lem  12658  isprm5  12659  phibndlem  12733  phibnd  12734  dfphi2  12737  hashdvds  12738  pclemdc  12806  pcaddlem  12857  pcmptdvds  12863  pcfac  12868  expnprm  12871  fngsum  13416  igsumvalx  13417  gsumval2  13425  gsumsplit1r  13426  gsumfzz  13523  plycoeid3  15425  relogbval  15619  relogbzcl  15620  nnlogbexp  15627  logblt  15630  logbgcd1irr  15635  lgsne0  15711  gausslemma2dlem4  15737  lgsquad2lem2  15755  2sqlem6  15793  2sqlem8a  15795  2sqlem8  15796  supfz  16398