Theorem eluzelz 10452

Description: A member of a set of upper 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 10450	. 2 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2	1	simp2bi 973	1 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1721   class class class wbr 4172   ` cfv 5413   <_ cle 9077   ZZcz 10238   ZZ>=cuz 10444

This theorem is referenced by:  eluzelre  10453  uztrn  10458  uzneg  10460  uzss  10462  eluzp1l  10466  eluzaddi  10468  eluzsubi  10469  uzm1  10472  uzin  10474  uzp1  10475  peano2uzr  10488  uzaddcl  10489  uzind4  10490  uzwo  10495  uzwoOLD  10496  uz2mulcl  10509  uzsupss  10524  elfz5  11007  elfzel2  11013  elfzelz  11015  eluzfz2  11021  peano2fzr  11025  fzsplit2  11032  fzopth  11045  fzsuc  11052  uzsplit  11073  uzdisj  11074  fzm1  11082  uznfz  11085  elfzo3  11110  fzoss2  11118  fzouzsplit  11123  fzofzp1b  11145  fzosplitsn  11150  om2uzlti  11245  om2uzf1oi  11248  uzrdgxfr  11261  fzen2  11263  seqm1  11295  seqfveq2  11300  seqfeq2  11301  seqshft2  11304  monoord  11308  monoord2  11309  sermono  11310  seqsplit  11311  seqf1olem1  11317  seqf1olem2  11318  seqid  11323  seqz  11326  leexp2a  11390  expnlbnd2  11465  expmulnbnd  11466  bcval5  11564  hashfz  11647  fzsdom2  11648  hashfzo  11649  seqcoll  11667  shftuz  11839  seqshft  11855  rexuz3  12107  r19.2uz  12110  rexuzre  12111  cau4  12115  caubnd2  12116  clim  12243  climrlim2  12296  climshftlem  12323  climshft  12325  climshft2  12331  climaddc1  12383  climmulc2  12385  climsubc1  12386  climsubc2  12387  clim2ser  12403  clim2ser2  12404  iserex  12405  climlec2  12407  climub  12410  isercolllem2  12414  isercoll  12416  isercoll2  12417  climcau  12419  caurcvg2  12426  caucvgb  12428  serf0  12429  iseraltlem1  12430  iseraltlem2  12431  iseralt  12433  sumrblem  12460  fsumcvg  12461  summolem2a  12464  fsumcvg2  12476  fsumm1  12492  fzosump1  12493  fsump1  12495  fsumrev2  12520  fsumtscopo  12536  fsumparts  12540  isumshft  12574  isumsplit  12575  isumrpcl  12578  isumsup2  12581  cvgrat  12615  mertenslem1  12616  dvdsexp  12860  isprm3  13043  nprm  13048  dvdsprm  13054  exprmfct  13065  isprm5  13067  maxprmfct  13068  phibndlem  13114  dfphi2  13118  hashdvds  13119  pclem  13167  pcaddlem  13212  pcfac  13223  expnprm  13226  prmreclem4  13242  vdwlem8  13311  gsumval2a  14737  efgtlen  15313  efgs1b  15323  iscau4  19185  caucfil  19189  iscmet3lem3  19196  iscmet3lem1  19197  iscmet3lem2  19198  lmle  19207  uniioombllem3  19430  mbflimsup  19511  mbfi1fseqlem6  19565  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  aaliou3lem1  20212  aaliou3lem2  20213  ulmres  20257  ulmshftlem  20258  ulmshft  20259  ulmcaulem  20263  ulmcau  20264  ulmdvlem1  20269  radcnvlem1  20282  dvradcnv  20290  muval1  20869  chtdif  20894  ppidif  20899  chtub  20949  bcmono  21014  bpos1lem  21019  lgsquad2lem2  21096  2sqlem6  21106  2sqlem8a  21108  2sqlem8  21109  chebbnd1lem1  21116  dchrisumlem2  21137  dchrisum0lem1  21163  ostthlem2  21275  ostth2  21284  constr3trllem3  21592  fzspl  24102  logblt  24359  supfz  25152  divcnvlin  25165  clim2div  25170  prodeq2ii  25192  fprodcvg  25209  prodmolem2a  25213  zprod  25216  fprodntriv  25221  fprodser  25228  fprodm1  25243  fprodp1  25245  fprodeq0  25252  preduz  25414  axlowdimlem3  25787  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  nn0prpwlem  26215  fdc  26339  mettrifi  26353  caushft  26357  rmspecsqrnq  26859  rmspecnonsq  26860  rmspecfund  26862  rmxyadd  26874  rmxy1  26875  rmxm1  26887  rmxluc  26889  rmyluc2  26891  jm2.17a  26915  jm2.18  26949  jm2.22  26956  jm2.15nn0  26964  jm2.16nn0  26965  jm2.27a  26966  jm2.27c  26968  jm3.1lem2  26979  jm3.1lem3  26980  jm3.1  26981  expdiophlem1  26982  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climsuselem1  27600  climsuse  27601  itgsinexp  27616  fzosplitsnm1  27991  elfzonelfzo  27992  iswrd0i  27999  swrdccatin12  28026

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-cnex 9002  ax-resscn 9003

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421  df-ov 6043  df-neg 9250  df-z 10239  df-uz 10445