Theorem eluzelz 11202

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

Syntax hints:   -> wi 4   e. wcel 1898   class class class wbr 4418   ` cfv 5605   <_ cle 9707   ZZcz 10971   ZZ>=cuz 11193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-cnex 9626  ax-resscn 9627

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-fv 5613  df-ov 6323  df-neg 9894  df-z 10972  df-uz 11194

This theorem is referenced by:  eluzelre  11203  uztrn  11209  uzneg  11211  uzss  11213  eluzp1l  11217  eluzaddi  11219  eluzsubi  11220  uzm1  11223  uzin  11225  uzind4  11251  uzwo  11256  uz2mulcl  11270  uzsupss  11290  elfz5  11827  elfzel2  11833  elfzelz  11835  eluzfz2  11842  peano2fzr  11847  fzsplit2  11859  fzopth  11870  fzsuc  11878  uzsplit  11901  uzdisj  11902  fzm1  11909  uznfz  11912  nn0disj  11943  preduz  11948  elfzo3  11973  fzoss2  11983  fzouzsplit  11990  eluzgtdifelfzo  12013  fzosplitsnm1  12025  fzofzp1b  12046  elfzonelfzo  12048  fzosplitsn  12054  fzisfzounsn  12057  modaddmodup  12191  om2uzlti  12202  om2uzf1oi  12205  uzrdgxfr  12218  fzen2  12220  seqfveq2  12273  seqfeq2  12274  seqshft2  12277  monoord  12281  monoord2  12282  sermono  12283  seqsplit  12284  seqf1olem1  12290  seqf1olem2  12291  seqid  12296  seqz  12299  leexp2a  12366  expnlbnd2  12441  expmulnbnd  12442  hashfz  12638  fzsdom2  12639  hashfzo  12640  seqcoll  12666  swrdfv2  12845  swrdccatin12  12890  rexuz3  13466  r19.2uz  13469  rexuzre  13470  cau4  13474  caubnd2  13475  clim  13613  climrlim2  13666  climshft2  13701  climaddc1  13753  climmulc2  13755  climsubc1  13756  climsubc2  13757  clim2ser  13773  clim2ser2  13774  iserex  13775  climlec2  13777  climub  13780  isercolllem2  13784  isercoll  13786  isercoll2  13787  climcau  13789  caurcvg2  13799  caucvgb  13801  serf0  13802  iseraltlem1  13803  iseraltlem2  13804  iseralt  13806  sumrblem  13832  fsumcvg  13833  summolem2a  13836  fsumcvg2  13848  fsumm1  13867  fzosump1  13868  fsump1  13872  fsumrev2  13898  telfsumo  13917  fsumparts  13921  isumsplit  13953  isumrpcl  13956  isumsup2  13959  cvgrat  13994  mertenslem1  13995  clim2div  14000  prodeq2ii  14022  fprodcvg  14039  prodmolem2a  14043  zprod  14046  fprodntriv  14051  fprodser  14058  fprodm1  14076  fprodp1  14078  fprodeq0  14084  isprm3  14688  nprm  14693  dvdsprm  14702  exprmfct  14703  isprm5  14706  maxprmfct  14707  ncoprmlnprm  14732  phibndlem  14773  dfphi2  14777  hashdvds  14778  pcaddlem  14888  pcfac  14899  expnprm  14902  prmreclem4  14918  vdwlem8  14993  gsumval2a  16577  efgs1b  17441  telgsumfzs  17674  iscau4  22304  caucfil  22308  iscmet3lem3  22315  iscmet3lem1  22316  iscmet3lem2  22317  lmle  22326  uniioombllem3  22599  mbflimsup  22679  mbflimsupOLD  22680  mbfi1fseqlem6  22734  dvfsumle  23029  dvfsumge  23030  dvfsumabs  23031  aaliou3lem1  23354  aaliou3lem2  23355  ulmres  23399  ulmshftlem  23400  ulmshft  23401  ulmcaulem  23405  ulmcau  23406  ulmdvlem1  23411  radcnvlem1  23424  logblt  23777  muval1  24116  chtdif  24141  ppidif  24146  chtub  24196  bcmono  24261  bpos1lem  24266  lgsquad2lem2  24343  2sqlem6  24353  2sqlem8a  24355  2sqlem8  24356  chebbnd1lem1  24363  dchrisumlem2  24384  dchrisum0lem1  24410  ostthlem2  24522  ostth2  24531  axlowdimlem3  25030  axlowdimlem6  25033  axlowdimlem7  25034  axlowdimlem16  25043  axlowdimlem17  25044  axlowdim  25047  constr3trllem3  25436  extwwlkfablem2  25862  fzspl  28420  fzdif2  28421  supfz  30412  divcnvlin  30417  nn0prpwlem  31028  fdc  32120  mettrifi  32132  caushft  32136  rmspecnonsq  35801  rmspecfund  35803  rmxyadd  35815  rmxy1  35816  jm2.18  35889  jm2.22  35896  jm2.15nn0  35904  jm2.16nn0  35905  jm2.27a  35906  jm2.27c  35908  jm3.1lem2  35919  jm3.1lem3  35920  jm3.1  35921  expdiophlem1  35922  dvgrat  36706  cvgdvgrat  36707  hashnzfz  36714  uzwo4  37431  monoords  37589  fzdifsuc2  37605  iuneqfzuzlem  37632  fmul01  37744  fmul01lt1lem1  37748  fmul01lt1lem2  37749  climsuselem1  37772  climsuse  37773  climf  37788  itgsinexp  37917  iblspltprt  37936  itgspltprt  37942  iundjiunlem  38402  iundjiun  38403  smonoord  38853  fzopredsuc  38855  iccpartiltu  38871  gboage9  39000  nnsum3primesle9  39024  nnsum4primesevenALTV  39031  wtgoldbnnsum4prm  39032  bgoldbnnsum3prm  39034  bgoldbtbndlem2  39036  pfxccatin12  39103  m1modmmod  40693  fllogbd  40740  fllog2  40748  dignn0ldlem  40782  dignnld  40783  digexp  40787  dignn0flhalf  40798  nn0sumshdiglemB  40800