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	|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Proof of Theorem eluzelz

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

Syntax hints:   -> wi 4   e. wcel 2200   class class class wbr 4083   ` cfv 5318   <_ cle 8193   ZZcz 9457   ZZ>=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  11211  pfxccatin12  11281  seq3shft  11365  rexuz3  11517  r19.2uz  11520  cau4  11643  caubnd2  11644  clim  11808  climshft2  11833  climaddc1  11856  climmulc2  11858  climsubc1  11859  climsubc2  11860  clim2ser  11864  clim2ser2  11865  iserex  11866  climlec2  11868  climub  11871  climcau  11874  climcaucn  11878  serf0  11879  sumrbdclem  11904  fsum3cvg  11905  summodclem2a  11908  zsumdc  11911  fsum3  11914  fisumss  11919  fsum3cvg2  11921  fsum3ser  11924  fsumcl2lem  11925  fsumadd  11933  fsumm1  11943  fzosump1  11944  fsum1p  11945  fsump1  11947  fsummulc2  11975  telfsumo  11993  fsumparts  11997  iserabs  12002  binomlem  12010  isumshft  12017  isumsplit  12018  isumrpcl  12021  divcnv  12024  trireciplem  12027  geosergap  12033  geolim2  12039  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemsumlt  12055  cvgratnnlemrate  12057  cvgratz  12059  cvgratgt0  12060  mertenslemi1  12062  clim2divap  12067  prodrbdclem  12098  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodntrivap  12111  fprodssdc  12117  fprodm1  12125  fprod1p  12126  fprodp1  12127  fprodabs  12143  fprodeq0  12144  efgt1p2  12222  modm1div  12327  dvdsbnd  12493  uzwodc  12574  ncoprmgcdne1b  12627  isprm3  12656  prmind2  12658  nprm  12661  dvdsprm  12675  exprmfct  12676  isprm5lem  12679  isprm5  12680  phibndlem  12754  phibnd  12755  dfphi2  12758  hashdvds  12759  pclemdc  12827  pcaddlem  12878  pcmptdvds  12884  pcfac  12889  expnprm  12892  fngsum  13437  igsumvalx  13438  gsumval2  13446  gsumsplit1r  13447  gsumfzz  13544  plycoeid3  15447  relogbval  15641  relogbzcl  15642  nnlogbexp  15649  logblt  15652  logbgcd1irr  15657  lgsne0  15733  gausslemma2dlem4  15759  lgsquad2lem2  15777  2sqlem6  15815  2sqlem8a  15817  2sqlem8  15818  supfz  16527