Theorem eluzelz 11176

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 11173	. 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 1872   class class class wbr 4423   ` cfv 5601   <_ cle 9684   ZZcz 10945   ZZ>=cuz 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-cnex 9603  ax-resscn 9604

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 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6309  df-neg 9871  df-z 10946  df-uz 11168

This theorem is referenced by:  eluzelre  11177  uztrn  11183  uzneg  11185  uzss  11187  eluzp1l  11191  eluzaddi  11193  eluzsubi  11194  uzm1  11197  uzin  11199  uzind4  11225  uzwo  11230  uz2mulcl  11244  uzsupss  11264  elfz5  11800  elfzel2  11806  elfzelz  11808  eluzfz2  11815  peano2fzr  11820  fzsplit2  11832  fzopth  11843  fzsuc  11851  uzsplit  11874  uzdisj  11875  fzm1  11882  uznfz  11885  nn0disj  11915  preduz  11919  elfzo3  11944  fzoss2  11954  fzouzsplit  11961  eluzgtdifelfzo  11983  fzosplitsnm1  11995  fzofzp1b  12016  elfzonelfzo  12018  fzosplitsn  12024  fzisfzounsn  12027  modaddmodup  12160  om2uzlti  12171  om2uzf1oi  12174  uzrdgxfr  12187  fzen2  12189  seqfveq2  12242  seqfeq2  12243  seqshft2  12246  monoord  12250  monoord2  12251  sermono  12252  seqsplit  12253  seqf1olem1  12259  seqf1olem2  12260  seqid  12265  seqz  12268  leexp2a  12335  expnlbnd2  12410  expmulnbnd  12411  hashfz  12604  fzsdom2  12605  hashfzo  12606  seqcoll  12632  swrdfv2  12805  swrdccatin12  12850  rexuz3  13412  r19.2uz  13415  rexuzre  13416  cau4  13420  caubnd2  13421  clim  13558  climrlim2  13611  climshft2  13646  climaddc1  13698  climmulc2  13700  climsubc1  13701  climsubc2  13702  clim2ser  13718  clim2ser2  13719  iserex  13720  climlec2  13722  climub  13725  isercolllem2  13729  isercoll  13731  isercoll2  13732  climcau  13734  caurcvg2  13744  caucvgb  13746  serf0  13747  iseraltlem1  13748  iseraltlem2  13749  iseralt  13751  sumrblem  13777  fsumcvg  13778  summolem2a  13781  fsumcvg2  13793  fsumm1  13812  fzosump1  13813  fsump1  13817  fsumrev2  13843  telfsumo  13862  fsumparts  13866  isumsplit  13898  isumrpcl  13901  isumsup2  13904  cvgrat  13939  mertenslem1  13940  clim2div  13945  prodeq2ii  13967  fprodcvg  13984  prodmolem2a  13988  zprod  13991  fprodntriv  13996  fprodser  14003  fprodm1  14021  fprodp1  14023  fprodeq0  14029  isprm3  14633  nprm  14638  dvdsprm  14647  exprmfct  14648  isprm5  14651  maxprmfct  14652  ncoprmlnprm  14677  phibndlem  14718  dfphi2  14722  hashdvds  14723  pcaddlem  14833  pcfac  14844  expnprm  14847  prmreclem4  14863  vdwlem8  14938  gsumval2a  16522  efgs1b  17386  telgsumfzs  17619  iscau4  22248  caucfil  22252  iscmet3lem3  22259  iscmet3lem1  22260  iscmet3lem2  22261  lmle  22270  uniioombllem3  22542  mbflimsup  22622  mbflimsupOLD  22623  mbfi1fseqlem6  22677  dvfsumle  22972  dvfsumge  22973  dvfsumabs  22974  aaliou3lem1  23297  aaliou3lem2  23298  ulmres  23342  ulmshftlem  23343  ulmshft  23344  ulmcaulem  23348  ulmcau  23349  ulmdvlem1  23354  radcnvlem1  23367  logblt  23720  muval1  24059  chtdif  24084  ppidif  24089  chtub  24139  bcmono  24204  bpos1lem  24209  lgsquad2lem2  24286  2sqlem6  24296  2sqlem8a  24298  2sqlem8  24299  chebbnd1lem1  24306  dchrisumlem2  24327  dchrisum0lem1  24353  ostthlem2  24465  ostth2  24474  axlowdimlem3  24973  axlowdimlem6  24976  axlowdimlem7  24977  axlowdimlem16  24986  axlowdimlem17  24987  axlowdim  24990  constr3trllem3  25379  extwwlkfablem2  25805  fzspl  28375  fzdif2  28376  supfz  30370  divcnvlin  30375  nn0prpwlem  30984  fdc  32039  mettrifi  32051  caushft  32055  rmspecnonsq  35726  rmspecfund  35728  rmxyadd  35740  rmxy1  35741  jm2.18  35814  jm2.22  35821  jm2.15nn0  35829  jm2.16nn0  35830  jm2.27a  35831  jm2.27c  35833  jm3.1lem2  35844  jm3.1lem3  35845  jm3.1  35846  expdiophlem1  35847  dvgrat  36632  cvgdvgrat  36633  hashnzfz  36640  uzwo4  37366  monoords  37469  fzdifsuc2  37485  iuneqfzuzlem  37512  fmul01  37599  fmul01lt1lem1  37603  fmul01lt1lem2  37604  climsuselem1  37627  climsuse  37628  climf  37643  itgsinexp  37772  iblspltprt  37791  itgspltprt  37797  iundjiunlem  38206  iundjiun  38207  smonoord  38589  fzopredsuc  38591  iccpartiltu  38607  gboage9  38736  nnsum3primesle9  38760  nnsum4primesevenALTV  38767  wtgoldbnnsum4prm  38768  bgoldbnnsum3prm  38770  bgoldbtbndlem2  38772  pfxccatin12  38837  m1modmmod  39975  fllogbd  40022  fllog2  40030  dignn0ldlem  40064  dignnld  40065  digexp  40069  dignn0flhalf  40080  nn0sumshdiglemB  40082