Theorem eluzelz 9659

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzelz	|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 9656	. 2 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2	1	simp2bi 1016	1 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2176   class class class wbr 4045   ` cfv 5272   <_ cle 8110   ZZcz 9374   ZZ>=cuz 9650

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254  ax-cnex 8018  ax-resscn 8019

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-opab 4107  df-mpt 4108  df-id 4341  df-xp 4682  df-rel 4683  df-cnv 4684  df-co 4685  df-dm 4686  df-rn 4687  df-res 4688  df-ima 4689  df-iota 5233  df-fun 5274  df-fn 5275  df-f 5276  df-fv 5280  df-ov 5949  df-neg 8248  df-z 9375  df-uz 9651

This theorem is referenced by:  eluzelre  9660  uztrn  9667  uzneg  9669  uzssz  9670  uzss  9671  eluzp1l  9675  eluzaddi  9677  eluzsubi  9678  eluzadd  9679  eluzsub  9680  uzm1  9681  uzin  9683  uzind4  9711  uz2mulcl  9731  elfz5  10141  elfzel2  10147  elfzelz  10149  eluzfz2  10156  peano2fzr  10161  fzsplit2  10174  fzopth  10185  fzsuc  10193  elfzp1  10196  fzdifsuc  10205  uzsplit  10216  uzdisj  10217  fzm1  10224  fzneuz  10225  uznfz  10227  nn0disj  10262  elfzo3  10288  fzoss2  10298  fzouzsplit  10305  eluzgtdifelfzo  10328  fzosplitsnm1  10340  fzofzp1b  10359  elfzonelfzo  10361  fzosplitsn  10364  fzisfzounsn  10367  zsupcllemstep  10374  infssuzex  10378  suprzubdc  10381  fldiv4lem1div2uz2  10451  mulp1mod1  10512  m1modge3gt1  10518  frec2uzltd  10550  frecfzen2  10574  uzennn  10583  uzsinds  10591  seq3fveq2  10622  seq3feq2  10623  seqfveq2g  10624  seq3shft2  10628  seqshft2g  10629  monoord  10632  monoord2  10633  ser3mono  10634  seq3split  10635  seqsplitg  10636  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  seq3f1olemqsumk  10659  seq3f1olemp  10662  seq3f1oleml  10663  seq3f1o  10664  seqf1oglem1  10666  seqf1oglem2  10667  seqf1og  10668  seq3id  10672  seq3z  10675  fser0const  10682  leexp2a  10739  expnlbnd2  10812  hashfz  10968  hashfzo  10969  hashfzp1  10971  seq3coll  10989  swrdfv2  11119  seq3shft  11182  rexuz3  11334  r19.2uz  11337  cau4  11460  caubnd2  11461  clim  11625  climshft2  11650  climaddc1  11673  climmulc2  11675  climsubc1  11676  climsubc2  11677  clim2ser  11681  clim2ser2  11682  iserex  11683  climlec2  11685  climub  11688  climcau  11691  climcaucn  11695  serf0  11696  sumrbdclem  11721  fsum3cvg  11722  summodclem2a  11725  zsumdc  11728  fsum3  11731  fisumss  11736  fsum3cvg2  11738  fsum3ser  11741  fsumcl2lem  11742  fsumadd  11750  fsumm1  11760  fzosump1  11761  fsum1p  11762  fsump1  11764  fsummulc2  11792  telfsumo  11810  fsumparts  11814  iserabs  11819  binomlem  11827  isumshft  11834  isumsplit  11835  isumrpcl  11838  divcnv  11841  trireciplem  11844  geosergap  11850  geolim2  11856  cvgratnnlemseq  11870  cvgratnnlemabsle  11871  cvgratnnlemsumlt  11872  cvgratnnlemrate  11874  cvgratz  11876  cvgratgt0  11877  mertenslemi1  11879  clim2divap  11884  prodrbdclem  11915  fproddccvg  11916  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodntrivap  11928  fprodssdc  11934  fprodm1  11942  fprod1p  11943  fprodp1  11944  fprodabs  11960  fprodeq0  11961  efgt1p2  12039  modm1div  12144  dvdsbnd  12310  uzwodc  12391  ncoprmgcdne1b  12444  isprm3  12473  prmind2  12475  nprm  12478  dvdsprm  12492  exprmfct  12493  isprm5lem  12496  isprm5  12497  phibndlem  12571  phibnd  12572  dfphi2  12575  hashdvds  12576  pclemdc  12644  pcaddlem  12695  pcmptdvds  12701  pcfac  12706  expnprm  12709  fngsum  13253  igsumvalx  13254  gsumval2  13262  gsumsplit1r  13263  gsumfzz  13360  plycoeid3  15262  relogbval  15456  relogbzcl  15457  nnlogbexp  15464  logblt  15467  logbgcd1irr  15472  lgsne0  15548  gausslemma2dlem4  15574  lgsquad2lem2  15592  2sqlem6  15630  2sqlem8a  15632  2sqlem8  15633  supfz  16047