Theorem eluzelz 10857

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

Syntax hints:   -> wi 4   e. wcel 1755   class class class wbr 4280   ` cfv 5406   <_ cle 9406   ZZcz 10633   ZZ>=cuz 10848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-cnex 9325  ax-resscn 9326

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414  df-ov 6083  df-neg 9585  df-z 10634  df-uz 10849

This theorem is referenced by:  eluzelre  10858  uztrn  10864  uzneg  10866  uzss  10868  eluzp1l  10872  eluzaddi  10874  eluzsubi  10875  uzm1  10878  uzin  10880  uzp1  10881  peano2uzr  10897  uzaddcl  10898  uzind4  10899  uzwo  10904  uzwoOLD  10905  uz2mulcl  10919  uzsupss  10934  elfz5  11431  elfzel2  11437  elfzelz  11439  eluzfz2  11445  peano2fzr  11449  fzsplit2  11460  fzopth  11481  fzsuc  11488  uzsplit  11513  uzdisj  11514  fzm1  11523  uznfz  11526  elfzo3  11551  fzoss2  11560  fzouzsplit  11567  fzosplitsnm1  11591  fzofzp1b  11608  elfzonelfzo  11610  fzosplitsn  11616  modaddmodup  11745  om2uzlti  11756  om2uzf1oi  11759  uzrdgxfr  11772  fzen2  11774  seqm1  11806  seqfveq2  11811  seqfeq2  11812  seqshft2  11815  monoord  11819  monoord2  11820  sermono  11821  seqsplit  11822  seqf1olem1  11828  seqf1olem2  11829  seqid  11834  seqz  11837  leexp2a  11902  expnlbnd2  11978  expmulnbnd  11979  bcval5  12077  hashfz  12171  fzsdom2  12172  hashfzo  12173  seqcoll  12199  swrdccatin12  12365  shftuz  12541  seqshft  12557  rexuz3  12819  r19.2uz  12822  rexuzre  12823  cau4  12827  caubnd2  12828  clim  12955  climrlim2  13008  climshftlem  13035  climshft  13037  climshft2  13043  climaddc1  13095  climmulc2  13097  climsubc1  13098  climsubc2  13099  clim2ser  13115  clim2ser2  13116  iserex  13117  climlec2  13119  climub  13122  isercolllem2  13126  isercoll  13128  isercoll2  13129  climcau  13131  caurcvg2  13138  caucvgb  13140  serf0  13141  iseraltlem1  13142  iseraltlem2  13143  iseralt  13145  sumrblem  13171  fsumcvg  13172  summolem2a  13175  fsumcvg2  13187  fsumm1  13203  fzosump1  13204  fsump1  13206  fsumrev2  13231  fsumtscopo  13247  fsumparts  13251  isumshft  13284  isumsplit  13285  isumrpcl  13288  isumsup2  13291  cvgrat  13325  mertenslem1  13326  dvdsexp  13571  isprm3  13754  nprm  13759  dvdsprm  13767  exprmfct  13778  isprm5  13780  maxprmfct  13781  phibndlem  13827  dfphi2  13831  hashdvds  13832  pclem  13887  pcaddlem  13932  pcfac  13943  expnprm  13946  prmreclem4  13962  vdwlem8  14031  gsumval2a  15491  efgtlen  16202  efgs1b  16212  iscau4  20631  caucfil  20635  iscmet3lem3  20642  iscmet3lem1  20643  iscmet3lem2  20644  lmle  20653  uniioombllem3  20906  mbflimsup  20985  mbfi1fseqlem6  21039  dvfsumle  21334  dvfsumge  21335  dvfsumabs  21336  aaliou3lem1  21692  aaliou3lem2  21693  ulmres  21737  ulmshftlem  21738  ulmshft  21739  ulmcaulem  21743  ulmcau  21744  ulmdvlem1  21749  radcnvlem1  21762  dvradcnv  21770  muval1  22355  chtdif  22380  ppidif  22385  chtub  22435  bcmono  22500  bpos1lem  22505  lgsquad2lem2  22582  2sqlem6  22592  2sqlem8a  22594  2sqlem8  22595  chebbnd1lem1  22602  dchrisumlem2  22623  dchrisum0lem1  22649  ostthlem2  22761  ostth2  22770  axlowdimlem3  23012  axlowdimlem6  23015  axlowdimlem7  23016  axlowdimlem16  23025  axlowdimlem17  23026  axlowdim  23029  constr3trllem3  23360  fzspl  25899  logblt  26318  supfz  27232  divcnvlin  27245  clim2div  27250  prodeq2ii  27272  fprodcvg  27289  prodmolem2a  27293  zprod  27296  fprodntriv  27301  fprodser  27308  fprodm1  27323  fprodp1  27325  fprodeq0  27332  preduz  27507  nn0prpwlem  28358  fdc  28482  mettrifi  28494  caushft  28498  rmspecsqrnq  29089  rmspecnonsq  29090  rmspecfund  29092  rmxyadd  29104  rmxy1  29105  rmxm1  29117  rmxluc  29119  rmyluc2  29121  jm2.17a  29145  jm2.18  29179  jm2.22  29186  jm2.15nn0  29194  jm2.16nn0  29195  jm2.27a  29196  jm2.27c  29198  jm3.1lem2  29209  jm3.1lem3  29210  jm3.1  29211  expdiophlem1  29212  fmul01  29603  fmul01lt1lem1  29607  fmul01lt1lem2  29608  climsuselem1  29623  climsuse  29624  itgsinexp  29638  fzisfzounsn  30054  eluzgtdifelfzo  30062  extwwlkfablem2  30514