Theorem eluzelz 11028

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

Syntax hints:   -> wi 4   e. wcel 1836   class class class wbr 4380   ` cfv 5509   <_ cle 9558   ZZcz 10799   ZZ>=cuz 11019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-cnex 9477  ax-resscn 9478

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-fv 5517  df-ov 6217  df-neg 9739  df-z 10800  df-uz 11020

This theorem is referenced by:  eluzelre  11029  uztrn  11035  uzneg  11037  uzss  11039  eluzp1l  11043  eluzaddi  11045  eluzsubi  11046  uzm1  11049  uzin  11051  uzind4  11077  uzwo  11082  uz2mulcl  11096  uzsupss  11111  elfz5  11619  elfzel2  11625  elfzelz  11627  eluzfz2  11633  peano2fzr  11638  fzsplit2  11649  fzopth  11660  fzsuc  11667  uzsplit  11690  uzdisj  11691  fzm1  11698  uznfz  11701  nn0disj  11731  elfzo3  11756  fzoss2  11766  fzouzsplit  11773  eluzgtdifelfzo  11795  fzosplitsnm1  11807  fzofzp1b  11828  elfzonelfzo  11830  fzosplitsn  11836  fzisfzounsn  11839  modaddmodup  11972  om2uzlti  11983  om2uzf1oi  11986  uzrdgxfr  11999  fzen2  12001  seqfveq2  12051  seqfeq2  12052  seqshft2  12055  monoord  12059  monoord2  12060  sermono  12061  seqsplit  12062  seqf1olem1  12068  seqf1olem2  12069  seqid  12074  seqz  12077  leexp2a  12143  expnlbnd2  12218  expmulnbnd  12219  hashfz  12408  fzsdom2  12409  hashfzo  12410  seqcoll  12435  swrdfv2  12601  swrdccatin12  12646  rexuz3  13202  r19.2uz  13205  rexuzre  13206  cau4  13210  caubnd2  13211  clim  13338  climrlim2  13391  climshft2  13426  climaddc1  13478  climmulc2  13480  climsubc1  13481  climsubc2  13482  clim2ser  13498  clim2ser2  13499  iserex  13500  climlec2  13502  climub  13505  isercolllem2  13509  isercoll  13511  isercoll2  13512  climcau  13514  caurcvg2  13521  caucvgb  13523  serf0  13524  iseraltlem1  13525  iseraltlem2  13526  iseralt  13528  sumrblem  13554  fsumcvg  13555  summolem2a  13558  fsumcvg2  13570  fsumm1  13587  fzosump1  13588  fsump1  13592  fsumrev2  13618  telfsumo  13637  fsumparts  13641  isumsplit  13673  isumrpcl  13676  isumsup2  13679  cvgrat  13713  mertenslem1  13714  clim2div  13719  prodeq2ii  13741  fprodcvg  13758  prodmolem2a  13762  zprod  13765  fprodntriv  13770  fprodser  13777  fprodm1  13792  fprodp1  13794  fprodeq0  13800  isprm3  14247  nprm  14252  dvdsprm  14261  exprmfct  14272  isprm5  14274  maxprmfct  14275  phibndlem  14321  dfphi2  14325  hashdvds  14326  pcaddlem  14428  pcfac  14439  expnprm  14442  prmreclem4  14458  vdwlem8  14527  gsumval2a  16042  efgs1b  16890  telgsumfzs  17150  iscau4  21822  caucfil  21826  iscmet3lem3  21833  iscmet3lem1  21834  iscmet3lem2  21835  lmle  21844  uniioombllem3  22098  mbflimsup  22177  mbfi1fseqlem6  22231  dvfsumle  22526  dvfsumge  22527  dvfsumabs  22528  aaliou3lem1  22842  aaliou3lem2  22843  ulmres  22887  ulmshftlem  22888  ulmshft  22889  ulmcaulem  22893  ulmcau  22894  ulmdvlem1  22899  radcnvlem1  22912  logblt  23261  muval1  23543  chtdif  23568  ppidif  23573  chtub  23623  bcmono  23688  bpos1lem  23693  lgsquad2lem2  23770  2sqlem6  23780  2sqlem8a  23782  2sqlem8  23783  chebbnd1lem1  23790  dchrisumlem2  23811  dchrisum0lem1  23837  ostthlem2  23949  ostth2  23958  axlowdimlem3  24389  axlowdimlem6  24392  axlowdimlem7  24393  axlowdimlem16  24402  axlowdimlem17  24403  axlowdim  24406  constr3trllem3  24794  extwwlkfablem2  25220  fzspl  27781  supfz  29309  divcnvlin  29320  preduz  29481  nn0prpwlem  30342  fdc  30440  mettrifi  30452  caushft  30456  rmspecnonsq  31044  rmspecfund  31046  rmxyadd  31058  rmxy1  31059  jm2.18  31132  jm2.22  31139  jm2.15nn0  31147  jm2.16nn0  31148  jm2.27a  31149  jm2.27c  31151  jm3.1lem2  31162  jm3.1lem3  31163  jm3.1  31164  expdiophlem1  31165  dvgrat  31397  cvgdvgrat  31398  hashnzfz  31429  monoords  31697  fzdifsuc2  31713  fmul01  31775  fmul01lt1lem1  31779  fmul01lt1lem2  31780  climsuselem1  31814  climsuse  31815  climf  31829  itgsinexp  31954  iblspltprt  31973  itgspltprt  31979  pfxccatin12  32635  m1modmmod  33369  fllogbd  33416  fllog2  33424  dignn0ldlem  33458  dignnld  33459  digexp  33463  dignn0flhalf  33474  nn0sumshdiglemB  33476