Theorem eluzelz 9535

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

Syntax hints:   -> wi 4   e. wcel 2148   class class class wbr 4003   ` cfv 5216   <_ cle 7991   ZZcz 9251   ZZ>=cuz 9526

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 4121  ax-pow 4174  ax-pr 4209  ax-cnex 7901  ax-resscn 7902

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 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-mpt 4066  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-fv 5224  df-ov 5877  df-neg 8129  df-z 9252  df-uz 9527

This theorem is referenced by:  eluzelre  9536  uztrn  9542  uzneg  9544  uzssz  9545  uzss  9546  eluzp1l  9550  eluzaddi  9552  eluzsubi  9553  eluzadd  9554  eluzsub  9555  uzm1  9556  uzin  9558  uzind4  9586  uz2mulcl  9606  elfz5  10014  elfzel2  10020  elfzelz  10022  eluzfz2  10029  peano2fzr  10034  fzsplit2  10047  fzopth  10058  fzsuc  10066  elfzp1  10069  fzdifsuc  10078  uzsplit  10089  uzdisj  10090  fzm1  10097  fzneuz  10098  uznfz  10100  nn0disj  10135  elfzo3  10160  fzoss2  10169  fzouzsplit  10176  eluzgtdifelfzo  10194  fzosplitsnm1  10206  fzofzp1b  10225  elfzonelfzo  10227  fzosplitsn  10230  fzisfzounsn  10233  mulp1mod1  10362  m1modge3gt1  10368  frec2uzltd  10400  frecfzen2  10424  uzennn  10433  uzsinds  10439  seq3fveq2  10466  seq3feq2  10467  seq3shft2  10470  monoord  10473  monoord2  10474  ser3mono  10475  seq3split  10476  iseqf1olemjpcl  10492  iseqf1olemqpcl  10493  seq3f1olemqsumk  10496  seq3f1olemp  10499  seq3f1oleml  10500  seq3f1o  10501  seq3id  10505  seq3z  10508  fser0const  10513  leexp2a  10570  expnlbnd2  10642  hashfz  10796  hashfzo  10797  hashfzp1  10799  seq3coll  10817  seq3shft  10842  rexuz3  10994  r19.2uz  10997  cau4  11120  caubnd2  11121  clim  11284  climshft2  11309  climaddc1  11332  climmulc2  11334  climsubc1  11335  climsubc2  11336  clim2ser  11340  clim2ser2  11341  iserex  11342  climlec2  11344  climub  11347  climcau  11350  climcaucn  11354  serf0  11355  sumrbdclem  11380  fsum3cvg  11381  summodclem2a  11384  zsumdc  11387  fsum3  11390  fisumss  11395  fsum3cvg2  11397  fsum3ser  11400  fsumcl2lem  11401  fsumadd  11409  fsumm1  11419  fzosump1  11420  fsum1p  11421  fsump1  11423  fsummulc2  11451  telfsumo  11469  fsumparts  11473  iserabs  11478  binomlem  11486  isumshft  11493  isumsplit  11494  isumrpcl  11497  divcnv  11500  trireciplem  11503  geosergap  11509  geolim2  11515  cvgratnnlemseq  11529  cvgratnnlemabsle  11530  cvgratnnlemsumlt  11531  cvgratnnlemrate  11533  cvgratz  11535  cvgratgt0  11536  mertenslemi1  11538  clim2divap  11543  prodrbdclem  11574  fproddccvg  11575  prodmodclem3  11578  prodmodclem2a  11579  zproddc  11582  fprodntrivap  11587  fprodssdc  11593  fprodm1  11601  fprod1p  11602  fprodp1  11603  fprodabs  11619  fprodeq0  11620  efgt1p2  11698  modm1div  11802  zsupcllemstep  11940  infssuzex  11944  suprzubdc  11947  dvdsbnd  11951  uzwodc  12032  ncoprmgcdne1b  12083  isprm3  12112  prmind2  12114  nprm  12117  dvdsprm  12131  exprmfct  12132  isprm5lem  12135  isprm5  12136  phibndlem  12210  phibnd  12211  dfphi2  12214  hashdvds  12215  pclemdc  12282  pcaddlem  12332  pcmptdvds  12337  pcfac  12342  expnprm  12345  relogbval  14300  relogbzcl  14301  nnlogbexp  14308  logblt  14311  logbgcd1irr  14316  lgsne0  14370  2sqlem6  14387  2sqlem8a  14389  2sqlem8  14390  supfz  14738