Theorem eluzelz 9764

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

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4088  ‘cfv 5326   ≤ cle 8214  ℤcz 9478  ℤ_≥cuz 9754

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-cnex 8122  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479  df-uz 9755

This theorem is referenced by:  eluzelre  9765  uztrn  9772  uzneg  9774  uzssz  9775  uzss  9776  eluzp1l  9780  eluzaddi  9782  eluzsubi  9783  eluzadd  9784  eluzsub  9785  uzm1  9786  uzin  9788  uzind4  9821  uz2mulcl  9841  elfz5  10251  elfzel2  10257  elfzelz  10259  eluzfz2  10266  peano2fzr  10271  fzsplit2  10284  fzopth  10295  fzsuc  10303  elfzp1  10306  fzdifsuc  10315  uzsplit  10326  uzdisj  10327  fzm1  10334  fzneuz  10335  uznfz  10337  nn0disj  10372  elfzo3  10398  fzoss2  10408  fzouzsplit  10415  fzoun  10417  eluzgtdifelfzo  10441  fzosplitsnm1  10453  fzofzp1b  10472  elfzonelfzo  10474  fzosplitsn  10477  fzisfzounsn  10481  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  fldiv4lem1div2uz2  10565  mulp1mod1  10626  m1modge3gt1  10632  frec2uzltd  10664  frecfzen2  10688  uzennn  10697  uzsinds  10705  seq3fveq2  10736  seq3feq2  10737  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  monoord2  10747  ser3mono  10748  seq3split  10749  seqsplitg  10750  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seq3f1olemqsumk  10773  seq3f1olemp  10776  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  seq3id  10786  seq3z  10789  fser0const  10796  leexp2a  10853  expnlbnd2  10926  hashfz  11084  hashfzo  11085  hashfzp1  11087  seq3coll  11105  swrdfv2  11243  pfxccatin12  11313  seq3shft  11398  rexuz3  11550  r19.2uz  11553  cau4  11676  caubnd2  11677  clim  11841  climshft2  11866  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  clim2ser  11897  clim2ser2  11898  iserex  11899  climlec2  11901  climub  11904  climcau  11907  climcaucn  11911  serf0  11912  sumrbdclem  11937  fsum3cvg  11938  summodclem2a  11941  zsumdc  11944  fsum3  11947  fisumss  11952  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumadd  11966  fsumm1  11976  fzosump1  11977  fsum1p  11978  fsump1  11980  fsummulc2  12008  telfsumo  12026  fsumparts  12030  iserabs  12035  binomlem  12043  isumshft  12050  isumsplit  12051  isumrpcl  12054  divcnv  12057  trireciplem  12060  geosergap  12066  geolim2  12072  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratnnlemrate  12090  cvgratz  12092  cvgratgt0  12093  mertenslemi1  12095  clim2divap  12100  prodrbdclem  12131  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodntrivap  12144  fprodssdc  12150  fprodm1  12158  fprod1p  12159  fprodp1  12160  fprodabs  12176  fprodeq0  12177  efgt1p2  12255  modm1div  12360  dvdsbnd  12526  uzwodc  12607  ncoprmgcdne1b  12660  isprm3  12689  prmind2  12691  nprm  12694  dvdsprm  12708  exprmfct  12709  isprm5lem  12712  isprm5  12713  phibndlem  12787  phibnd  12788  dfphi2  12791  hashdvds  12792  pclemdc  12860  pcaddlem  12911  pcmptdvds  12917  pcfac  12922  expnprm  12925  fngsum  13470  igsumvalx  13471  gsumval2  13479  gsumsplit1r  13480  gsumfzz  13577  plycoeid3  15480  relogbval  15674  relogbzcl  15675  nnlogbexp  15682  logblt  15685  logbgcd1irr  15690  lgsne0  15766  gausslemma2dlem4  15792  lgsquad2lem2  15810  2sqlem6  15848  2sqlem8a  15850  2sqlem8  15851  supfz  16675  gsumgfsumlem  16683