Theorem eluzelz 9826

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

Syntax hints:   -> wi 4   e. wcel 2202   class class class wbr 4093   ` cfv 5333   <_ cle 8274   ZZcz 9540   ZZ>=cuz 9816

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-cnex 8183  ax-resscn 8184

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341  df-ov 6031  df-neg 8412  df-z 9541  df-uz 9817

This theorem is referenced by:  eluzelre  9827  uztrn  9834  uzneg  9836  uzssz  9837  uzss  9838  eluzp1l  9842  eluzaddi  9844  eluzsubi  9845  eluzadd  9846  eluzsub  9847  uzm1  9848  uzin  9850  uzind4  9883  uz2mulcl  9903  elfz5  10314  elfzel2  10320  elfzelz  10322  eluzfz2  10329  peano2fzr  10334  fzsplit2  10347  fzopth  10358  fzsuc  10366  elfzp1  10369  fzdifsuc  10378  uzsplit  10389  uzdisj  10390  fzm1  10397  fzneuz  10398  uznfz  10400  nn0disj  10435  elfzo3  10461  fzoss2  10471  fzouzsplit  10478  fzoun  10480  eluzgtdifelfzo  10505  fzosplitsnm1  10517  fzofzp1b  10536  elfzonelfzo  10538  fzosplitsn  10541  fzisfzounsn  10545  zsupcllemstep  10552  infssuzex  10556  suprzubdc  10559  fldiv4lem1div2uz2  10629  mulp1mod1  10690  m1modge3gt1  10696  frec2uzltd  10728  frecfzen2  10752  uzennn  10761  uzsinds  10769  seq3fveq2  10800  seq3feq2  10801  seqfveq2g  10802  seq3shft2  10806  seqshft2g  10807  monoord  10810  monoord2  10811  ser3mono  10812  seq3split  10813  seqsplitg  10814  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  seq3f1olemqsumk  10837  seq3f1olemp  10840  seq3f1oleml  10841  seq3f1o  10842  seqf1oglem1  10844  seqf1oglem2  10845  seqf1og  10846  seq3id  10850  seq3z  10853  fser0const  10860  leexp2a  10917  expnlbnd2  10990  hashfz  11148  hashfzo  11149  hashfzp1  11151  seq3coll  11169  swrdfv2  11310  pfxccatin12  11380  seq3shft  11478  rexuz3  11630  r19.2uz  11633  cau4  11756  caubnd2  11757  clim  11921  climshft2  11946  climaddc1  11969  climmulc2  11971  climsubc1  11972  climsubc2  11973  clim2ser  11977  clim2ser2  11978  iserex  11979  climlec2  11981  climub  11984  climcau  11987  climcaucn  11991  serf0  11992  sumrbdclem  12018  fsum3cvg  12019  summodclem2a  12022  zsumdc  12025  fsum3  12028  fisumss  12033  fsum3cvg2  12035  fsum3ser  12038  fsumcl2lem  12039  fsumadd  12047  fsumm1  12057  fzosump1  12058  fsum1p  12059  fsump1  12061  fsummulc2  12089  telfsumo  12107  fsumparts  12111  iserabs  12116  binomlem  12124  isumshft  12131  isumsplit  12132  isumrpcl  12135  divcnv  12138  trireciplem  12141  geosergap  12147  geolim2  12153  cvgratnnlemseq  12167  cvgratnnlemabsle  12168  cvgratnnlemsumlt  12169  cvgratnnlemrate  12171  cvgratz  12173  cvgratgt0  12174  mertenslemi1  12176  clim2divap  12181  prodrbdclem  12212  fproddccvg  12213  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodntrivap  12225  fprodssdc  12231  fprodm1  12239  fprod1p  12240  fprodp1  12241  fprodabs  12257  fprodeq0  12258  efgt1p2  12336  modm1div  12441  dvdsbnd  12607  uzwodc  12688  ncoprmgcdne1b  12741  isprm3  12770  prmind2  12772  nprm  12775  dvdsprm  12789  exprmfct  12790  isprm5lem  12793  isprm5  12794  phibndlem  12868  phibnd  12869  dfphi2  12872  hashdvds  12873  pclemdc  12941  pcaddlem  12992  pcmptdvds  12998  pcfac  13003  expnprm  13006  fngsum  13551  igsumvalx  13552  gsumval2  13560  gsumsplit1r  13561  gsumfzz  13658  plycoeid3  15568  relogbval  15762  relogbzcl  15763  nnlogbexp  15770  logblt  15773  logbgcd1irr  15778  lgsne0  15857  gausslemma2dlem4  15883  lgsquad2lem2  15901  2sqlem6  15939  2sqlem8a  15941  2sqlem8  15942  supfz  16804  gsumgfsumlem  16812