Theorem eluzelz 11697

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

Syntax hints:   -> wi 4   e. wcel 1990   class class class wbr 4653   ` cfv 5888   <_ cle 10075   ZZcz 11377   ZZ>=cuz 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378  df-uz 11688

This theorem is referenced by:  eluzelre  11698  uztrn  11704  uzneg  11706  uzss  11708  eluzp1l  11712  eluzaddi  11714  eluzsubi  11715  uzm1  11718  uzin  11720  uzind4  11746  uzwo  11751  uz2mulcl  11766  uzsupss  11780  elfz5  12334  elfzel2  12340  elfzelz  12342  eluzfz2  12349  peano2fzr  12354  fzsplit2  12366  fzopth  12378  ssfzunsn  12387  fzsuc  12388  elfz1uz  12410  uzsplit  12412  uzdisj  12413  fzm1  12420  uznfz  12423  nn0disj  12455  preduz  12461  elfzo3  12486  fzoss2  12496  fzouzsplit  12503  eluzgtdifelfzo  12529  fzosplitsnm1  12542  fzofzp1b  12566  elfzonelfzo  12570  fzosplitsn  12576  fzisfzounsn  12580  fldiv4lem1div2uz2  12637  m1modge3gt1  12717  modaddmodup  12733  om2uzlti  12749  om2uzf1oi  12752  uzrdgxfr  12766  fzen2  12768  seqfveq2  12823  seqfeq2  12824  seqshft2  12827  monoord  12831  monoord2  12832  sermono  12833  seqsplit  12834  seqf1olem1  12840  seqf1olem2  12841  seqid  12846  seqz  12849  leexp2a  12916  expnlbnd2  12995  expmulnbnd  12996  hashfz  13214  fzsdom2  13215  hashfzo  13216  hashfzp1  13218  seqcoll  13248  swrdfv2  13446  swrdccatin12  13491  rexuz3  14088  r19.2uz  14091  rexuzre  14092  cau4  14096  caubnd2  14097  clim  14225  climrlim2  14278  climshft2  14313  climaddc1  14365  climmulc2  14367  climsubc1  14368  climsubc2  14369  clim2ser  14385  clim2ser2  14386  iserex  14387  climlec2  14389  climub  14392  isercolllem2  14396  isercoll  14398  isercoll2  14399  climcau  14401  caurcvg2  14408  caucvgb  14410  serf0  14411  iseraltlem1  14412  iseraltlem2  14413  iseralt  14415  sumrblem  14442  fsumcvg  14443  summolem2a  14446  fsumcvg2  14458  fsumm1  14480  fzosump1  14481  fsump1  14487  fsumrev2  14514  telfsumo  14534  fsumparts  14538  isumsplit  14572  isumrpcl  14575  isumsup2  14578  cvgrat  14615  mertenslem1  14616  clim2div  14621  prodeq2ii  14643  fprodcvg  14660  prodmolem2a  14664  zprod  14667  fprodntriv  14672  fprodser  14679  fprodm1  14697  fprodp1  14699  fprodeq0  14705  isprm3  15396  nprm  15401  dvdsprm  15415  exprmfct  15416  isprm5  15419  maxprmfct  15421  ncoprmlnprm  15436  phibndlem  15475  dfphi2  15479  hashdvds  15480  pcaddlem  15592  pcfac  15603  expnprm  15606  prmreclem4  15623  vdwlem8  15692  gsumval2a  17279  efgs1b  18149  telgsumfzs  18386  iscau4  23077  caucfil  23081  iscmet3lem3  23088  iscmet3lem1  23089  iscmet3lem2  23090  lmle  23099  uniioombllem3  23353  mbflimsup  23433  mbfi1fseqlem6  23487  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  aaliou3lem1  24097  aaliou3lem2  24098  ulmres  24142  ulmshftlem  24143  ulmshft  24144  ulmcaulem  24148  ulmcau  24149  ulmdvlem1  24154  radcnvlem1  24167  logblt  24522  muval1  24859  chtdif  24884  ppidif  24889  chtub  24937  bcmono  25002  bpos1lem  25007  lgsquad2lem2  25110  2sqlem6  25148  2sqlem8a  25150  2sqlem8  25151  chebbnd1lem1  25158  dchrisumlem2  25179  dchrisum0lem1  25205  ostthlem2  25317  ostth2  25326  axlowdimlem3  25824  axlowdimlem6  25827  axlowdimlem7  25828  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  extwwlkfablem2  27210  fzspl  29550  fzdif2  29551  supfz  31613  divcnvlin  31618  nn0prpwlem  32317  fdc  33541  mettrifi  33553  caushft  33557  rmspecnonsq  37472  rmspecfund  37474  rmxyadd  37486  rmxy1  37487  jm2.18  37555  jm2.22  37562  jm2.15nn0  37570  jm2.16nn0  37571  jm2.27a  37572  jm2.27c  37574  jm3.1lem2  37585  jm3.1lem3  37586  jm3.1  37587  expdiophlem1  37588  dvgrat  38511  cvgdvgrat  38512  hashnzfz  38519  uzwo4  39221  ssinc  39264  ssdec  39265  rexanuz3  39275  monoords  39511  fzdifsuc2  39525  iuneqfzuzlem  39550  eluzelzd  39591  allbutfi  39616  eluzelz2  39627  uzid2  39630  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  climsuselem1  39839  climsuse  39840  climf  39854  climresmpt  39891  climf2  39898  limsupequzlem  39954  limsupmnfuzlem  39958  limsupre3uzlem  39967  itgsinexp  40170  iblspltprt  40189  itgspltprt  40195  iundjiunlem  40676  iundjiun  40677  smflimsuplem2  41027  smflimsuplem4  41029  smflimsuplem5  41030  fzopredsuc  41333  smonoord  41341  iccpartiltu  41358  pfxccatin12  41425  fmtnoprmfac2lem1  41478  fmtnofac2lem  41480  lighneallem2  41523  lighneallem4a  41525  lighneallem4b  41526  gboge9  41652  nnsum3primesle9  41682  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem2  41694  m1modmmod  42316  fllogbd  42354  fllog2  42362  dignn0ldlem  42396  dignnld  42397  digexp  42401  dignn0flhalf  42412  nn0sumshdiglemB  42414