Theorem eluzelz 11090

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

Syntax hints:   -> wi 4   e. wcel 1767   class class class wbr 4447   ` cfv 5587   <_ cle 9628   ZZcz 10863   ZZ>=cuz 11081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-cnex 9547  ax-resscn 9548

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-fv 5595  df-ov 6286  df-neg 9807  df-z 10864  df-uz 11082

This theorem is referenced by:  eluzelre  11091  uztrn  11097  uzneg  11099  uzss  11101  eluzp1l  11105  eluzaddi  11107  eluzsubi  11108  uzm1  11111  uzin  11113  uzp1  11114  peano2uzr  11135  uzaddcl  11136  uzind4  11138  uzwo  11143  uzwoOLD  11144  uz2mulcl  11158  uzsupss  11173  elfz5  11679  elfzel2  11685  elfzelz  11687  eluzfz2  11693  peano2fzr  11698  fzsplit2  11709  fzopth  11719  fzsuc  11726  uzsplit  11749  uzdisj  11750  fzm1  11757  uznfz  11760  nn0disj  11787  elfzo3  11811  fzoss2  11820  fzouzsplit  11827  eluzgtdifelfzo  11845  fzosplitsnm1  11857  fzofzp1b  11877  elfzonelfzo  11879  fzosplitsn  11885  fzisfzounsn  11888  modaddmodup  12017  om2uzlti  12028  om2uzf1oi  12031  uzrdgxfr  12044  fzen2  12046  seqm1  12091  seqfveq2  12096  seqfeq2  12097  seqshft2  12100  monoord  12104  monoord2  12105  sermono  12106  seqsplit  12107  seqf1olem1  12113  seqf1olem2  12114  seqid  12119  seqz  12122  leexp2a  12188  expnlbnd2  12264  expmulnbnd  12265  bcval5  12363  hashfz  12449  fzsdom2  12450  hashfzo  12451  seqcoll  12477  swrdccatin12  12678  shftuz  12864  seqshft  12880  rexuz3  13143  r19.2uz  13146  rexuzre  13147  cau4  13151  caubnd2  13152  clim  13279  climrlim2  13332  climshftlem  13359  climshft  13361  climshft2  13367  climaddc1  13419  climmulc2  13421  climsubc1  13422  climsubc2  13423  clim2ser  13439  clim2ser2  13440  iserex  13441  climlec2  13443  climub  13446  isercolllem2  13450  isercoll  13452  isercoll2  13453  climcau  13455  caurcvg2  13462  caucvgb  13464  serf0  13465  iseraltlem1  13466  iseraltlem2  13467  iseralt  13469  sumrblem  13495  fsumcvg  13496  summolem2a  13499  fsumcvg2  13511  fsumm1  13528  fzosump1  13529  fsump1  13533  fsumrev2  13559  telfsumo  13578  fsumparts  13582  isumshft  13613  isumsplit  13614  isumrpcl  13617  isumsup2  13620  cvgrat  13654  mertenslem1  13655  dvdsexp  13900  isprm3  14084  nprm  14089  dvdsprm  14098  exprmfct  14109  isprm5  14111  maxprmfct  14112  phibndlem  14158  dfphi2  14162  hashdvds  14163  pclem  14220  pcaddlem  14265  pcfac  14276  expnprm  14279  prmreclem4  14295  vdwlem8  14364  gsumval2a  15831  efgtlen  16547  efgs1b  16557  telgsumfzs  16818  iscau4  21469  caucfil  21473  iscmet3lem3  21480  iscmet3lem1  21481  iscmet3lem2  21482  lmle  21491  uniioombllem3  21745  mbflimsup  21824  mbfi1fseqlem6  21878  dvfsumle  22173  dvfsumge  22174  dvfsumabs  22175  aaliou3lem1  22488  aaliou3lem2  22489  ulmres  22533  ulmshftlem  22534  ulmshft  22535  ulmcaulem  22539  ulmcau  22540  ulmdvlem1  22545  radcnvlem1  22558  dvradcnv  22566  muval1  23151  chtdif  23176  ppidif  23181  chtub  23231  bcmono  23296  bpos1lem  23301  lgsquad2lem2  23378  2sqlem6  23388  2sqlem8a  23390  2sqlem8  23391  chebbnd1lem1  23398  dchrisumlem2  23419  dchrisum0lem1  23445  ostthlem2  23557  ostth2  23566  axlowdimlem3  23939  axlowdimlem6  23942  axlowdimlem7  23943  axlowdimlem16  23952  axlowdimlem17  23953  axlowdim  23956  constr3trllem3  24344  extwwlkfablem2  24771  fzspl  27282  logblt  27678  supfz  28598  divcnvlin  28611  clim2div  28616  prodeq2ii  28638  fprodcvg  28655  prodmolem2a  28659  zprod  28662  fprodntriv  28667  fprodser  28674  fprodm1  28689  fprodp1  28691  fprodeq0  28698  preduz  28873  nn0prpwlem  29733  fdc  29857  mettrifi  29869  caushft  29873  rmspecsqrtnq  30462  rmspecnonsq  30463  rmspecfund  30465  rmxyadd  30477  rmxy1  30478  rmxm1  30490  rmxluc  30492  rmyluc2  30494  jm2.17a  30518  jm2.18  30550  jm2.22  30557  jm2.15nn0  30565  jm2.16nn0  30566  jm2.27a  30567  jm2.27c  30569  jm3.1lem2  30580  jm3.1lem3  30581  jm3.1  30582  expdiophlem1  30583  hashnzfz  30841  monoords  31089  fmul01  31146  fmul01lt1lem1  31150  fmul01lt1lem2  31151  climsuselem1  31165  climsuse  31166  climf  31180  itgsinexp  31288  iblspltprt  31307  itgspltprt  31313