Theorem eluzelz 9026

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

Syntax hints:   -> wi 4   e. wcel 1438   class class class wbr 3845   ` cfv 5015   <_ cle 7521   ZZcz 8748   ZZ>=cuz 9017

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036  ax-cnex 7434  ax-resscn 7435

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2841  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-br 3846  df-opab 3900  df-mpt 3901  df-id 4120  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-fv 5023  df-ov 5655  df-neg 7654  df-z 8749  df-uz 9018

This theorem is referenced by:  eluzelre  9027  uztrn  9033  uzneg  9035  uzssz  9036  uzss  9037  eluzp1l  9041  eluzaddi  9043  eluzsubi  9044  eluzadd  9045  eluzsub  9046  uzm1  9047  uzin  9049  uzind4  9074  uz2mulcl  9093  elfz5  9430  elfzel2  9436  elfzelz  9438  eluzfz2  9444  peano2fzr  9449  fzsplit2  9462  fzopth  9472  fzsuc  9479  elfzp1  9482  fzdifsuc  9491  uzsplit  9502  uzdisj  9503  fzm1  9510  fzneuz  9511  uznfz  9513  nn0disj  9545  elfzo3  9570  fzoss2  9579  fzouzsplit  9586  eluzgtdifelfzo  9604  fzosplitsnm1  9616  fzofzp1b  9635  elfzonelfzo  9637  fzosplitsn  9640  fzisfzounsn  9643  mulp1mod1  9768  m1modge3gt1  9774  frec2uzltd  9806  frecfzen2  9830  uzsinds  9844  iseqfveq2  9886  iseqfeq2  9887  seq3fveq2  9888  seq3feq2  9889  iseqshft2  9894  monoord  9900  monoord2  9901  isermono  9902  seq3split  9903  iseqsplit  9904  iseqf1olemjpcl  9920  iseqf1olemqpcl  9921  seq3f1olemqsumk  9924  seq3f1olemp  9927  seq3f1oleml  9928  seq3f1o  9929  iseqid  9935  iseqz  9939  fser0const  9947  leexp2a  10004  expnlbnd2  10075  hashfz  10225  hashfzo  10226  hashfzp1  10228  iseqcoll  10243  seq3shft  10268  rexuz3  10419  r19.2uz  10422  cau4  10545  caubnd2  10546  clim  10665  climshft2  10691  climaddc1  10713  climmulc2  10715  climsubc1  10716  climsubc2  10717  clim2ser  10721  clim2ser2  10722  iserex  10723  climlec2  10726  climub  10729  climcau  10732  climcaucn  10736  serf0  10737  isumrblem  10761  fisumcvg  10762  fsum3cvg  10763  isummolem2a  10767  zisum  10770  fisum  10774  fsum3  10775  fisumss  10780  fisumcvg2  10782  fsum3cvg2  10783  fisumser  10786  fsumcl2lem  10788  fsumadd  10796  fsumm1  10806  fzosump1  10807  fsum1p  10808  fsump1  10810  fsummulc2  10838  telfsumo  10856  fsumparts  10860  iserabs  10865  binomlem  10873  isumshft  10880  isumsplit  10881  isumrpcl  10884  divcnv  10887  trireciplem  10890  geosergap  10896  geolim2  10902  cvgratnnlemseq  10916  cvgratnnlemabsle  10917  cvgratnnlemsumlt  10918  cvgratnnlemrate  10920  cvgratz  10922  cvgratgt0  10923  mertenslemi1  10925  efgt1p2  10981  zsupcllemstep  11215  infssuzex  11219  dvdsbnd  11222  ncoprmgcdne1b  11345  isprm3  11374  prmind2  11376  nprm  11379  dvdsprm  11392  exprmfct  11393  phibndlem  11466  phibnd  11467  dfphi2  11470  hashdvds  11471  supfz  11871