Theorem eluzelz 9765

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 9761	. 2 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2	1	simp2bi 1039	1 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2202   class class class wbr 4088   ` cfv 5326   <_ cle 8215   ZZcz 9479   ZZ>=cuz 9755

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 8123  ax-resscn 8124

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 6021  df-neg 8353  df-z 9480  df-uz 9756

This theorem is referenced by:  eluzelre  9766  uztrn  9773  uzneg  9775  uzssz  9776  uzss  9777  eluzp1l  9781  eluzaddi  9783  eluzsubi  9784  eluzadd  9785  eluzsub  9786  uzm1  9787  uzin  9789  uzind4  9822  uz2mulcl  9842  elfz5  10252  elfzel2  10258  elfzelz  10260  eluzfz2  10267  peano2fzr  10272  fzsplit2  10285  fzopth  10296  fzsuc  10304  elfzp1  10307  fzdifsuc  10316  uzsplit  10327  uzdisj  10328  fzm1  10335  fzneuz  10336  uznfz  10338  nn0disj  10373  elfzo3  10399  fzoss2  10409  fzouzsplit  10416  fzoun  10418  eluzgtdifelfzo  10443  fzosplitsnm1  10455  fzofzp1b  10474  elfzonelfzo  10476  fzosplitsn  10479  fzisfzounsn  10483  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  fldiv4lem1div2uz2  10567  mulp1mod1  10628  m1modge3gt1  10634  frec2uzltd  10666  frecfzen2  10690  uzennn  10699  uzsinds  10707  seq3fveq2  10738  seq3feq2  10739  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsumk  10775  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  fser0const  10798  leexp2a  10855  expnlbnd2  10928  hashfz  11086  hashfzo  11087  hashfzp1  11089  seq3coll  11107  swrdfv2  11248  pfxccatin12  11318  seq3shft  11416  rexuz3  11568  r19.2uz  11571  cau4  11694  caubnd2  11695  clim  11859  climshft2  11884  climaddc1  11907  climmulc2  11909  climsubc1  11910  climsubc2  11911  clim2ser  11915  clim2ser2  11916  iserex  11917  climlec2  11919  climub  11922  climcau  11925  climcaucn  11929  serf0  11930  sumrbdclem  11956  fsum3cvg  11957  summodclem2a  11960  zsumdc  11963  fsum3  11966  fisumss  11971  fsum3cvg2  11973  fsum3ser  11976  fsumcl2lem  11977  fsumadd  11985  fsumm1  11995  fzosump1  11996  fsum1p  11997  fsump1  11999  fsummulc2  12027  telfsumo  12045  fsumparts  12049  iserabs  12054  binomlem  12062  isumshft  12069  isumsplit  12070  isumrpcl  12073  divcnv  12076  trireciplem  12079  geosergap  12085  geolim2  12091  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratnnlemrate  12109  cvgratz  12111  cvgratgt0  12112  mertenslemi1  12114  clim2divap  12119  prodrbdclem  12150  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodntrivap  12163  fprodssdc  12169  fprodm1  12177  fprod1p  12178  fprodp1  12179  fprodabs  12195  fprodeq0  12196  efgt1p2  12274  modm1div  12379  dvdsbnd  12545  uzwodc  12626  ncoprmgcdne1b  12679  isprm3  12708  prmind2  12710  nprm  12713  dvdsprm  12727  exprmfct  12728  isprm5lem  12731  isprm5  12732  phibndlem  12806  phibnd  12807  dfphi2  12810  hashdvds  12811  pclemdc  12879  pcaddlem  12930  pcmptdvds  12936  pcfac  12941  expnprm  12944  fngsum  13489  igsumvalx  13490  gsumval2  13498  gsumsplit1r  13499  gsumfzz  13596  plycoeid3  15500  relogbval  15694  relogbzcl  15695  nnlogbexp  15702  logblt  15705  logbgcd1irr  15710  lgsne0  15786  gausslemma2dlem4  15812  lgsquad2lem2  15830  2sqlem6  15868  2sqlem8a  15870  2sqlem8  15871  supfz  16727  gsumgfsumlem  16735