Theorem eluzelz 9743

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

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4083  ‘cfv 5318   ≤ cle 8193  ℤcz 9457  ℤ_≥cuz 9733

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 4202  ax-pow 4258  ax-pr 4293  ax-cnex 8101  ax-resscn 8102

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 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458  df-uz 9734

This theorem is referenced by:  eluzelre  9744  uztrn  9751  uzneg  9753  uzssz  9754  uzss  9755  eluzp1l  9759  eluzaddi  9761  eluzsubi  9762  eluzadd  9763  eluzsub  9764  uzm1  9765  uzin  9767  uzind4  9795  uz2mulcl  9815  elfz5  10225  elfzel2  10231  elfzelz  10233  eluzfz2  10240  peano2fzr  10245  fzsplit2  10258  fzopth  10269  fzsuc  10277  elfzp1  10280  fzdifsuc  10289  uzsplit  10300  uzdisj  10301  fzm1  10308  fzneuz  10309  uznfz  10311  nn0disj  10346  elfzo3  10372  fzoss2  10382  fzouzsplit  10389  fzoun  10391  eluzgtdifelfzo  10415  fzosplitsnm1  10427  fzofzp1b  10446  elfzonelfzo  10448  fzosplitsn  10451  fzisfzounsn  10454  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  fldiv4lem1div2uz2  10538  mulp1mod1  10599  m1modge3gt1  10605  frec2uzltd  10637  frecfzen2  10661  uzennn  10670  uzsinds  10678  seq3fveq2  10709  seq3feq2  10710  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seq3f1olemqsumk  10746  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  seq3id  10759  seq3z  10762  fser0const  10769  leexp2a  10826  expnlbnd2  10899  hashfz  11056  hashfzo  11057  hashfzp1  11059  seq3coll  11077  swrdfv2  11210  pfxccatin12  11280  seq3shft  11364  rexuz3  11516  r19.2uz  11519  cau4  11642  caubnd2  11643  clim  11807  climshft2  11832  climaddc1  11855  climmulc2  11857  climsubc1  11858  climsubc2  11859  clim2ser  11863  clim2ser2  11864  iserex  11865  climlec2  11867  climub  11870  climcau  11873  climcaucn  11877  serf0  11878  sumrbdclem  11903  fsum3cvg  11904  summodclem2a  11907  zsumdc  11910  fsum3  11913  fisumss  11918  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumadd  11932  fsumm1  11942  fzosump1  11943  fsum1p  11944  fsump1  11946  fsummulc2  11974  telfsumo  11992  fsumparts  11996  iserabs  12001  binomlem  12009  isumshft  12016  isumsplit  12017  isumrpcl  12020  divcnv  12023  trireciplem  12026  geosergap  12032  geolim2  12038  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemsumlt  12054  cvgratnnlemrate  12056  cvgratz  12058  cvgratgt0  12059  mertenslemi1  12061  clim2divap  12066  prodrbdclem  12097  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodntrivap  12110  fprodssdc  12116  fprodm1  12124  fprod1p  12125  fprodp1  12126  fprodabs  12142  fprodeq0  12143  efgt1p2  12221  modm1div  12326  dvdsbnd  12492  uzwodc  12573  ncoprmgcdne1b  12626  isprm3  12655  prmind2  12657  nprm  12660  dvdsprm  12674  exprmfct  12675  isprm5lem  12678  isprm5  12679  phibndlem  12753  phibnd  12754  dfphi2  12757  hashdvds  12758  pclemdc  12826  pcaddlem  12877  pcmptdvds  12883  pcfac  12888  expnprm  12891  fngsum  13436  igsumvalx  13437  gsumval2  13445  gsumsplit1r  13446  gsumfzz  13543  plycoeid3  15446  relogbval  15640  relogbzcl  15641  nnlogbexp  15648  logblt  15651  logbgcd1irr  15656  lgsne0  15732  gausslemma2dlem4  15758  lgsquad2lem2  15776  2sqlem6  15814  2sqlem8a  15816  2sqlem8  15817  supfz  16499