Theorem eluzelz 11101

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

Syntax hints:   -> wi 4   e. wcel 1804   class class class wbr 4437   ` cfv 5578   <_ cle 9632   ZZcz 10871   ZZ>=cuz 11092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-cnex 9551  ax-resscn 9552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-ov 6284  df-neg 9813  df-z 10872  df-uz 11093

This theorem is referenced by:  eluzelre  11102  uztrn  11108  uzneg  11110  uzss  11112  eluzp1l  11116  eluzaddi  11118  eluzsubi  11119  uzm1  11122  uzin  11124  uzind4  11150  uzwo  11155  uzwoOLD  11156  uz2mulcl  11170  uzsupss  11185  elfz5  11691  elfzel2  11697  elfzelz  11699  eluzfz2  11705  peano2fzr  11710  fzsplit2  11721  fzopth  11731  fzsuc  11738  uzsplit  11761  uzdisj  11762  fzm1  11769  uznfz  11772  nn0disj  11802  elfzo3  11826  fzoss2  11835  fzouzsplit  11842  eluzgtdifelfzo  11860  fzosplitsnm1  11872  fzofzp1b  11892  elfzonelfzo  11894  fzosplitsn  11900  fzisfzounsn  11903  modaddmodup  12032  om2uzlti  12043  om2uzf1oi  12046  uzrdgxfr  12059  fzen2  12061  seqfveq2  12111  seqfeq2  12112  seqshft2  12115  monoord  12119  monoord2  12120  sermono  12121  seqsplit  12122  seqf1olem1  12128  seqf1olem2  12129  seqid  12134  seqz  12137  leexp2a  12203  expnlbnd2  12279  expmulnbnd  12280  hashfz  12467  fzsdom2  12468  hashfzo  12469  seqcoll  12494  swrdccatin12  12698  rexuz3  13163  r19.2uz  13166  rexuzre  13167  cau4  13171  caubnd2  13172  clim  13299  climrlim2  13352  climshft2  13387  climaddc1  13439  climmulc2  13441  climsubc1  13442  climsubc2  13443  clim2ser  13459  clim2ser2  13460  iserex  13461  climlec2  13463  climub  13466  isercolllem2  13470  isercoll  13472  isercoll2  13473  climcau  13475  caurcvg2  13482  caucvgb  13484  serf0  13485  iseraltlem1  13486  iseraltlem2  13487  iseralt  13489  sumrblem  13515  fsumcvg  13516  summolem2a  13519  fsumcvg2  13531  fsumm1  13548  fzosump1  13549  fsump1  13553  fsumrev2  13579  telfsumo  13598  fsumparts  13602  isumsplit  13634  isumrpcl  13637  isumsup2  13640  cvgrat  13674  mertenslem1  13675  clim2div  13680  prodeq2ii  13702  fprodcvg  13719  prodmolem2a  13723  zprod  13726  fprodntriv  13731  fprodser  13738  fprodm1  13753  fprodp1  13755  fprodeq0  13761  isprm3  14208  nprm  14213  dvdsprm  14222  exprmfct  14233  isprm5  14235  maxprmfct  14236  phibndlem  14282  dfphi2  14286  hashdvds  14287  pcaddlem  14389  pcfac  14400  expnprm  14403  prmreclem4  14419  vdwlem8  14488  gsumval2a  15885  efgs1b  16733  telgsumfzs  16997  iscau4  21696  caucfil  21700  iscmet3lem3  21707  iscmet3lem1  21708  iscmet3lem2  21709  lmle  21718  uniioombllem3  21972  mbflimsup  22051  mbfi1fseqlem6  22105  dvfsumle  22400  dvfsumge  22401  dvfsumabs  22402  aaliou3lem1  22716  aaliou3lem2  22717  ulmres  22761  ulmshftlem  22762  ulmshft  22763  ulmcaulem  22767  ulmcau  22768  ulmdvlem1  22773  radcnvlem1  22786  muval1  23385  chtdif  23410  ppidif  23415  chtub  23465  bcmono  23530  bpos1lem  23535  lgsquad2lem2  23612  2sqlem6  23622  2sqlem8a  23624  2sqlem8  23625  chebbnd1lem1  23632  dchrisumlem2  23653  dchrisum0lem1  23679  ostthlem2  23791  ostth2  23800  axlowdimlem3  24225  axlowdimlem6  24228  axlowdimlem7  24229  axlowdimlem16  24238  axlowdimlem17  24239  axlowdim  24242  constr3trllem3  24630  extwwlkfablem2  25056  fzspl  27576  logblt  28000  supfz  29085  divcnvlin  29096  preduz  29256  nn0prpwlem  30116  fdc  30214  mettrifi  30226  caushft  30230  rmspecnonsq  30819  rmspecfund  30821  rmxyadd  30833  rmxy1  30834  jm2.18  30906  jm2.22  30913  jm2.15nn0  30921  jm2.16nn0  30922  jm2.27a  30923  jm2.27c  30925  jm3.1lem2  30936  jm3.1lem3  30937  jm3.1  30938  expdiophlem1  30939  dvgrat  31169  cvgdvgrat  31170  hashnzfz  31201  monoords  31450  fzdifsuc2  31466  fmul01  31528  fmul01lt1lem1  31532  fmul01lt1lem2  31533  climsuselem1  31567  climsuse  31568  climf  31582  itgsinexp  31707  iblspltprt  31726  itgspltprt  31732