Theorem eluzelz 11168

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

Syntax hints:   -> wi 4   e. wcel 1870   class class class wbr 4426   ` cfv 5601   <_ cle 9675   ZZcz 10937   ZZ>=cuz 11159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-cnex 9594  ax-resscn 9595

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6308  df-neg 9862  df-z 10938  df-uz 11160

This theorem is referenced by:  eluzelre  11169  uztrn  11175  uzneg  11177  uzss  11179  eluzp1l  11183  eluzaddi  11185  eluzsubi  11186  uzm1  11189  uzin  11191  uzind4  11217  uzwo  11222  uz2mulcl  11236  uzsupss  11256  elfz5  11790  elfzel2  11796  elfzelz  11798  eluzfz2  11805  peano2fzr  11810  fzsplit2  11822  fzopth  11833  fzsuc  11841  uzsplit  11864  uzdisj  11865  fzm1  11872  uznfz  11875  nn0disj  11905  preduz  11909  elfzo3  11934  fzoss2  11944  fzouzsplit  11951  eluzgtdifelfzo  11973  fzosplitsnm1  11985  fzofzp1b  12006  elfzonelfzo  12008  fzosplitsn  12014  fzisfzounsn  12017  modaddmodup  12150  om2uzlti  12161  om2uzf1oi  12164  uzrdgxfr  12177  fzen2  12179  seqfveq2  12232  seqfeq2  12233  seqshft2  12236  monoord  12240  monoord2  12241  sermono  12242  seqsplit  12243  seqf1olem1  12249  seqf1olem2  12250  seqid  12255  seqz  12258  leexp2a  12325  expnlbnd2  12400  expmulnbnd  12401  hashfz  12594  fzsdom2  12595  hashfzo  12596  seqcoll  12621  swrdfv2  12787  swrdccatin12  12832  rexuz3  13390  r19.2uz  13393  rexuzre  13394  cau4  13398  caubnd2  13399  clim  13536  climrlim2  13589  climshft2  13624  climaddc1  13676  climmulc2  13678  climsubc1  13679  climsubc2  13680  clim2ser  13696  clim2ser2  13697  iserex  13698  climlec2  13700  climub  13703  isercolllem2  13707  isercoll  13709  isercoll2  13710  climcau  13712  caurcvg2  13722  caucvgb  13724  serf0  13725  iseraltlem1  13726  iseraltlem2  13727  iseralt  13729  sumrblem  13755  fsumcvg  13756  summolem2a  13759  fsumcvg2  13771  fsumm1  13790  fzosump1  13791  fsump1  13795  fsumrev2  13821  telfsumo  13840  fsumparts  13844  isumsplit  13876  isumrpcl  13879  isumsup2  13882  cvgrat  13917  mertenslem1  13918  clim2div  13923  prodeq2ii  13945  fprodcvg  13962  prodmolem2a  13966  zprod  13969  fprodntriv  13974  fprodser  13981  fprodm1  13999  fprodp1  14001  fprodeq0  14007  isprm3  14604  nprm  14609  dvdsprm  14618  exprmfct  14619  isprm5  14622  maxprmfct  14623  ncoprmlnprm  14648  phibndlem  14687  dfphi2  14691  hashdvds  14692  pcaddlem  14796  pcfac  14807  expnprm  14810  prmreclem4  14826  vdwlem8  14901  gsumval2a  16473  efgs1b  17321  telgsumfzs  17554  iscau4  22142  caucfil  22146  iscmet3lem3  22153  iscmet3lem1  22154  iscmet3lem2  22155  lmle  22164  uniioombllem3  22420  mbflimsup  22500  mbflimsupOLD  22501  mbfi1fseqlem6  22555  dvfsumle  22850  dvfsumge  22851  dvfsumabs  22852  aaliou3lem1  23163  aaliou3lem2  23164  ulmres  23208  ulmshftlem  23209  ulmshft  23210  ulmcaulem  23214  ulmcau  23215  ulmdvlem1  23220  radcnvlem1  23233  logblt  23586  muval1  23923  chtdif  23948  ppidif  23953  chtub  24003  bcmono  24068  bpos1lem  24073  lgsquad2lem2  24150  2sqlem6  24160  2sqlem8a  24162  2sqlem8  24163  chebbnd1lem1  24170  dchrisumlem2  24191  dchrisum0lem1  24217  ostthlem2  24329  ostth2  24338  axlowdimlem3  24820  axlowdimlem6  24823  axlowdimlem7  24824  axlowdimlem16  24833  axlowdimlem17  24834  axlowdim  24837  constr3trllem3  25225  extwwlkfablem2  25651  fzspl  28204  fzdif2  28205  supfz  30149  divcnvlin  30154  nn0prpwlem  30763  fdc  31778  mettrifi  31790  caushft  31794  rmspecnonsq  35461  rmspecfund  35463  rmxyadd  35475  rmxy1  35476  jm2.18  35549  jm2.22  35556  jm2.15nn0  35564  jm2.16nn0  35565  jm2.27a  35566  jm2.27c  35568  jm3.1lem2  35579  jm3.1lem3  35580  jm3.1  35581  expdiophlem1  35582  dvgrat  36298  cvgdvgrat  36299  hashnzfz  36306  uzwo4  37033  monoords  37123  fzdifsuc2  37139  iuneqfzuzlem  37166  fmul01  37230  fmul01lt1lem1  37234  fmul01lt1lem2  37235  climsuselem1  37258  climsuse  37259  climf  37274  itgsinexp  37400  iblspltprt  37419  itgspltprt  37425  iundjiunlem  37806  iundjiun  37807  smonoord  38108  fzopredsuc  38110  iccpartiltu  38126  gboage9  38255  nnsum3primesle9  38279  nnsum4primesevenALTV  38286  wtgoldbnnsum4prm  38287  bgoldbnnsum3prm  38289  bgoldbtbndlem2  38291  pfxccatin12  38356  m1modmmod  39085  fllogbd  39132  fllog2  39140  dignn0ldlem  39174  dignnld  39175  digexp  39179  dignn0flhalf  39190  nn0sumshdiglemB  39192