Theorem eluzelz 9539

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

Syntax hints:   → wi 4   ∈ wcel 2148   class class class wbr 4005  ‘cfv 5218   ≤ cle 7995  ℤcz 9255  ℤ_≥cuz 9530

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-cnex 7904  ax-resscn 7905

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-fv 5226  df-ov 5880  df-neg 8133  df-z 9256  df-uz 9531

This theorem is referenced by:  eluzelre  9540  uztrn  9546  uzneg  9548  uzssz  9549  uzss  9550  eluzp1l  9554  eluzaddi  9556  eluzsubi  9557  eluzadd  9558  eluzsub  9559  uzm1  9560  uzin  9562  uzind4  9590  uz2mulcl  9610  elfz5  10019  elfzel2  10025  elfzelz  10027  eluzfz2  10034  peano2fzr  10039  fzsplit2  10052  fzopth  10063  fzsuc  10071  elfzp1  10074  fzdifsuc  10083  uzsplit  10094  uzdisj  10095  fzm1  10102  fzneuz  10103  uznfz  10105  nn0disj  10140  elfzo3  10165  fzoss2  10174  fzouzsplit  10181  eluzgtdifelfzo  10199  fzosplitsnm1  10211  fzofzp1b  10230  elfzonelfzo  10232  fzosplitsn  10235  fzisfzounsn  10238  mulp1mod1  10367  m1modge3gt1  10373  frec2uzltd  10405  frecfzen2  10429  uzennn  10438  uzsinds  10444  seq3fveq2  10471  seq3feq2  10472  seq3shft2  10475  monoord  10478  monoord2  10479  ser3mono  10480  seq3split  10481  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  seq3f1olemqsumk  10501  seq3f1olemp  10504  seq3f1oleml  10505  seq3f1o  10506  seq3id  10510  seq3z  10513  fser0const  10518  leexp2a  10575  expnlbnd2  10648  hashfz  10803  hashfzo  10804  hashfzp1  10806  seq3coll  10824  seq3shft  10849  rexuz3  11001  r19.2uz  11004  cau4  11127  caubnd2  11128  clim  11291  climshft2  11316  climaddc1  11339  climmulc2  11341  climsubc1  11342  climsubc2  11343  clim2ser  11347  clim2ser2  11348  iserex  11349  climlec2  11351  climub  11354  climcau  11357  climcaucn  11361  serf0  11362  sumrbdclem  11387  fsum3cvg  11388  summodclem2a  11391  zsumdc  11394  fsum3  11397  fisumss  11402  fsum3cvg2  11404  fsum3ser  11407  fsumcl2lem  11408  fsumadd  11416  fsumm1  11426  fzosump1  11427  fsum1p  11428  fsump1  11430  fsummulc2  11458  telfsumo  11476  fsumparts  11480  iserabs  11485  binomlem  11493  isumshft  11500  isumsplit  11501  isumrpcl  11504  divcnv  11507  trireciplem  11510  geosergap  11516  geolim2  11522  cvgratnnlemseq  11536  cvgratnnlemabsle  11537  cvgratnnlemsumlt  11538  cvgratnnlemrate  11540  cvgratz  11542  cvgratgt0  11543  mertenslemi1  11545  clim2divap  11550  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodntrivap  11594  fprodssdc  11600  fprodm1  11608  fprod1p  11609  fprodp1  11610  fprodabs  11626  fprodeq0  11627  efgt1p2  11705  modm1div  11809  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  dvdsbnd  11959  uzwodc  12040  ncoprmgcdne1b  12091  isprm3  12120  prmind2  12122  nprm  12125  dvdsprm  12139  exprmfct  12140  isprm5lem  12143  isprm5  12144  phibndlem  12218  phibnd  12219  dfphi2  12222  hashdvds  12223  pclemdc  12290  pcaddlem  12340  pcmptdvds  12345  pcfac  12350  expnprm  12353  relogbval  14408  relogbzcl  14409  nnlogbexp  14416  logblt  14419  logbgcd1irr  14424  lgsne0  14478  2sqlem6  14506  2sqlem8a  14508  2sqlem8  14509  supfz  14858