Theorem eluzelz 10984

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

Syntax hints:   -> wi 4   e. wcel 1758   class class class wbr 4403   ` cfv 5529   <_ cle 9533   ZZcz 10760   ZZ>=cuz 10975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-cnex 9452  ax-resscn 9453

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-fv 5537  df-ov 6206  df-neg 9712  df-z 10761  df-uz 10976

This theorem is referenced by:  eluzelre  10985  uztrn  10991  uzneg  10993  uzss  10995  eluzp1l  10999  eluzaddi  11001  eluzsubi  11002  uzm1  11005  uzin  11007  uzp1  11008  peano2uzr  11024  uzaddcl  11025  uzind4  11026  uzwo  11031  uzwoOLD  11032  uz2mulcl  11046  uzsupss  11061  elfz5  11565  elfzel2  11571  elfzelz  11573  eluzfz2  11579  peano2fzr  11583  fzsplit2  11594  fzopth  11615  fzsuc  11622  uzsplit  11650  uzdisj  11651  fzm1  11660  uznfz  11663  elfzo3  11688  fzoss2  11697  fzouzsplit  11704  fzosplitsnm1  11728  fzofzp1b  11745  elfzonelfzo  11747  fzosplitsn  11753  modaddmodup  11882  om2uzlti  11893  om2uzf1oi  11896  uzrdgxfr  11909  fzen2  11911  seqm1  11943  seqfveq2  11948  seqfeq2  11949  seqshft2  11952  monoord  11956  monoord2  11957  sermono  11958  seqsplit  11959  seqf1olem1  11965  seqf1olem2  11966  seqid  11971  seqz  11974  leexp2a  12039  expnlbnd2  12115  expmulnbnd  12116  bcval5  12214  hashfz  12309  fzsdom2  12310  hashfzo  12311  seqcoll  12337  swrdccatin12  12503  shftuz  12679  seqshft  12695  rexuz3  12957  r19.2uz  12960  rexuzre  12961  cau4  12965  caubnd2  12966  clim  13093  climrlim2  13146  climshftlem  13173  climshft  13175  climshft2  13181  climaddc1  13233  climmulc2  13235  climsubc1  13236  climsubc2  13237  clim2ser  13253  clim2ser2  13254  iserex  13255  climlec2  13257  climub  13260  isercolllem2  13264  isercoll  13266  isercoll2  13267  climcau  13269  caurcvg2  13276  caucvgb  13278  serf0  13279  iseraltlem1  13280  iseraltlem2  13281  iseralt  13283  sumrblem  13309  fsumcvg  13310  summolem2a  13313  fsumcvg2  13325  fsumm1  13341  fzosump1  13342  fsump1  13344  fsumrev2  13370  fsumtscopo  13386  fsumparts  13390  isumshft  13423  isumsplit  13424  isumrpcl  13427  isumsup2  13430  cvgrat  13464  mertenslem1  13465  dvdsexp  13710  isprm3  13893  nprm  13898  dvdsprm  13906  exprmfct  13917  isprm5  13919  maxprmfct  13920  phibndlem  13966  dfphi2  13970  hashdvds  13971  pclem  14026  pcaddlem  14071  pcfac  14082  expnprm  14085  prmreclem4  14101  vdwlem8  14170  gsumval2a  15634  efgtlen  16347  efgs1b  16357  iscau4  20925  caucfil  20929  iscmet3lem3  20936  iscmet3lem1  20937  iscmet3lem2  20938  lmle  20947  uniioombllem3  21201  mbflimsup  21280  mbfi1fseqlem6  21334  dvfsumle  21629  dvfsumge  21630  dvfsumabs  21631  aaliou3lem1  21944  aaliou3lem2  21945  ulmres  21989  ulmshftlem  21990  ulmshft  21991  ulmcaulem  21995  ulmcau  21996  ulmdvlem1  22001  radcnvlem1  22014  dvradcnv  22022  muval1  22607  chtdif  22632  ppidif  22637  chtub  22687  bcmono  22752  bpos1lem  22757  lgsquad2lem2  22834  2sqlem6  22844  2sqlem8a  22846  2sqlem8  22847  chebbnd1lem1  22854  dchrisumlem2  22875  dchrisum0lem1  22901  ostthlem2  23013  ostth2  23022  axlowdimlem3  23362  axlowdimlem6  23365  axlowdimlem7  23366  axlowdimlem16  23375  axlowdimlem17  23376  axlowdim  23379  constr3trllem3  23710  fzspl  26242  logblt  26630  supfz  27550  divcnvlin  27563  clim2div  27568  prodeq2ii  27590  fprodcvg  27607  prodmolem2a  27611  zprod  27614  fprodntriv  27619  fprodser  27626  fprodm1  27641  fprodp1  27643  fprodeq0  27650  preduz  27825  nn0prpwlem  28685  fdc  28809  mettrifi  28821  caushft  28825  rmspecsqrnq  29415  rmspecnonsq  29416  rmspecfund  29418  rmxyadd  29430  rmxy1  29431  rmxm1  29443  rmxluc  29445  rmyluc2  29447  jm2.17a  29471  jm2.18  29505  jm2.22  29512  jm2.15nn0  29520  jm2.16nn0  29521  jm2.27a  29522  jm2.27c  29524  jm3.1lem2  29535  jm3.1lem3  29536  jm3.1  29537  expdiophlem1  29538  fmul01  29929  fmul01lt1lem1  29933  fmul01lt1lem2  29934  climsuselem1  29948  climsuse  29949  itgsinexp  29963  fzisfzounsn  30379  eluzgtdifelfzo  30387  extwwlkfablem2  30839  nn0disj  30906  telescfzgsum  30982