Theorem eluzelz 9731

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 9728	. 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 8182   ZZcz 9446   ZZ>=cuz 9722

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 8090  ax-resscn 8091

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 6004  df-neg 8320  df-z 9447  df-uz 9723

This theorem is referenced by:  eluzelre  9732  uztrn  9739  uzneg  9741  uzssz  9742  uzss  9743  eluzp1l  9747  eluzaddi  9749  eluzsubi  9750  eluzadd  9751  eluzsub  9752  uzm1  9753  uzin  9755  uzind4  9783  uz2mulcl  9803  elfz5  10213  elfzel2  10219  elfzelz  10221  eluzfz2  10228  peano2fzr  10233  fzsplit2  10246  fzopth  10257  fzsuc  10265  elfzp1  10268  fzdifsuc  10277  uzsplit  10288  uzdisj  10289  fzm1  10296  fzneuz  10297  uznfz  10299  nn0disj  10334  elfzo3  10360  fzoss2  10370  fzouzsplit  10377  fzoun  10379  eluzgtdifelfzo  10403  fzosplitsnm1  10415  fzofzp1b  10434  elfzonelfzo  10436  fzosplitsn  10439  fzisfzounsn  10442  zsupcllemstep  10449  infssuzex  10453  suprzubdc  10456  fldiv4lem1div2uz2  10526  mulp1mod1  10587  m1modge3gt1  10593  frec2uzltd  10625  frecfzen2  10649  uzennn  10658  uzsinds  10666  seq3fveq2  10697  seq3feq2  10698  seqfveq2g  10699  seq3shft2  10703  seqshft2g  10704  monoord  10707  monoord2  10708  ser3mono  10709  seq3split  10710  seqsplitg  10711  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seq3f1olemqsumk  10734  seq3f1olemp  10737  seq3f1oleml  10738  seq3f1o  10739  seqf1oglem1  10741  seqf1oglem2  10742  seqf1og  10743  seq3id  10747  seq3z  10750  fser0const  10757  leexp2a  10814  expnlbnd2  10887  hashfz  11043  hashfzo  11044  hashfzp1  11046  seq3coll  11064  swrdfv2  11195  pfxccatin12  11265  seq3shft  11349  rexuz3  11501  r19.2uz  11504  cau4  11627  caubnd2  11628  clim  11792  climshft2  11817  climaddc1  11840  climmulc2  11842  climsubc1  11843  climsubc2  11844  clim2ser  11848  clim2ser2  11849  iserex  11850  climlec2  11852  climub  11855  climcau  11858  climcaucn  11862  serf0  11863  sumrbdclem  11888  fsum3cvg  11889  summodclem2a  11892  zsumdc  11895  fsum3  11898  fisumss  11903  fsum3cvg2  11905  fsum3ser  11908  fsumcl2lem  11909  fsumadd  11917  fsumm1  11927  fzosump1  11928  fsum1p  11929  fsump1  11931  fsummulc2  11959  telfsumo  11977  fsumparts  11981  iserabs  11986  binomlem  11994  isumshft  12001  isumsplit  12002  isumrpcl  12005  divcnv  12008  trireciplem  12011  geosergap  12017  geolim2  12023  cvgratnnlemseq  12037  cvgratnnlemabsle  12038  cvgratnnlemsumlt  12039  cvgratnnlemrate  12041  cvgratz  12043  cvgratgt0  12044  mertenslemi1  12046  clim2divap  12051  prodrbdclem  12082  fproddccvg  12083  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodntrivap  12095  fprodssdc  12101  fprodm1  12109  fprod1p  12110  fprodp1  12111  fprodabs  12127  fprodeq0  12128  efgt1p2  12206  modm1div  12311  dvdsbnd  12477  uzwodc  12558  ncoprmgcdne1b  12611  isprm3  12640  prmind2  12642  nprm  12645  dvdsprm  12659  exprmfct  12660  isprm5lem  12663  isprm5  12664  phibndlem  12738  phibnd  12739  dfphi2  12742  hashdvds  12743  pclemdc  12811  pcaddlem  12862  pcmptdvds  12868  pcfac  12873  expnprm  12876  fngsum  13421  igsumvalx  13422  gsumval2  13430  gsumsplit1r  13431  gsumfzz  13528  plycoeid3  15431  relogbval  15625  relogbzcl  15626  nnlogbexp  15633  logblt  15636  logbgcd1irr  15641  lgsne0  15717  gausslemma2dlem4  15743  lgsquad2lem2  15761  2sqlem6  15799  2sqlem8a  15801  2sqlem8  15802  supfz  16439