MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzelz Structured version   Unicode version

Theorem eluzelz 10862
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
StepHypRef Expression
1 eluz2 10859 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp2bi 1004 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   class class class wbr 4287   ` cfv 5413    <_ cle 9411   ZZcz 10638   ZZ>=cuz 10853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-cnex 9330  ax-resscn 9331
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639  df-uz 10854
This theorem is referenced by:  eluzelre  10863  uztrn  10869  uzneg  10871  uzss  10873  eluzp1l  10877  eluzaddi  10879  eluzsubi  10880  uzm1  10883  uzin  10885  uzp1  10886  peano2uzr  10902  uzaddcl  10903  uzind4  10904  uzwo  10909  uzwoOLD  10910  uz2mulcl  10924  uzsupss  10939  elfz5  11437  elfzel2  11443  elfzelz  11445  eluzfz2  11451  peano2fzr  11455  fzsplit2  11466  fzopth  11487  fzsuc  11494  uzsplit  11522  uzdisj  11523  fzm1  11532  uznfz  11535  elfzo3  11560  fzoss2  11569  fzouzsplit  11576  fzosplitsnm1  11600  fzofzp1b  11617  elfzonelfzo  11619  fzosplitsn  11625  modaddmodup  11754  om2uzlti  11765  om2uzf1oi  11768  uzrdgxfr  11781  fzen2  11783  seqm1  11815  seqfveq2  11820  seqfeq2  11821  seqshft2  11824  monoord  11828  monoord2  11829  sermono  11830  seqsplit  11831  seqf1olem1  11837  seqf1olem2  11838  seqid  11843  seqz  11846  leexp2a  11911  expnlbnd2  11987  expmulnbnd  11988  bcval5  12086  hashfz  12180  fzsdom2  12181  hashfzo  12182  seqcoll  12208  swrdccatin12  12374  shftuz  12550  seqshft  12566  rexuz3  12828  r19.2uz  12831  rexuzre  12832  cau4  12836  caubnd2  12837  clim  12964  climrlim2  13017  climshftlem  13044  climshft  13046  climshft2  13052  climaddc1  13104  climmulc2  13106  climsubc1  13107  climsubc2  13108  clim2ser  13124  clim2ser2  13125  iserex  13126  climlec2  13128  climub  13131  isercolllem2  13135  isercoll  13137  isercoll2  13138  climcau  13140  caurcvg2  13147  caucvgb  13149  serf0  13150  iseraltlem1  13151  iseraltlem2  13152  iseralt  13154  sumrblem  13180  fsumcvg  13181  summolem2a  13184  fsumcvg2  13196  fsumm1  13212  fzosump1  13213  fsump1  13215  fsumrev2  13241  fsumtscopo  13257  fsumparts  13261  isumshft  13294  isumsplit  13295  isumrpcl  13298  isumsup2  13301  cvgrat  13335  mertenslem1  13336  dvdsexp  13581  isprm3  13764  nprm  13769  dvdsprm  13777  exprmfct  13788  isprm5  13790  maxprmfct  13791  phibndlem  13837  dfphi2  13841  hashdvds  13842  pclem  13897  pcaddlem  13942  pcfac  13953  expnprm  13956  prmreclem4  13972  vdwlem8  14041  gsumval2a  15503  efgtlen  16214  efgs1b  16224  iscau4  20765  caucfil  20769  iscmet3lem3  20776  iscmet3lem1  20777  iscmet3lem2  20778  lmle  20787  uniioombllem3  21040  mbflimsup  21119  mbfi1fseqlem6  21173  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  aaliou3lem1  21783  aaliou3lem2  21784  ulmres  21828  ulmshftlem  21829  ulmshft  21830  ulmcaulem  21834  ulmcau  21835  ulmdvlem1  21840  radcnvlem1  21853  dvradcnv  21861  muval1  22446  chtdif  22471  ppidif  22476  chtub  22526  bcmono  22591  bpos1lem  22596  lgsquad2lem2  22673  2sqlem6  22683  2sqlem8a  22685  2sqlem8  22686  chebbnd1lem1  22693  dchrisumlem2  22714  dchrisum0lem1  22740  ostthlem2  22852  ostth2  22861  axlowdimlem3  23141  axlowdimlem6  23144  axlowdimlem7  23145  axlowdimlem16  23154  axlowdimlem17  23155  axlowdim  23158  constr3trllem3  23489  fzspl  26028  logblt  26417  supfz  27337  divcnvlin  27350  clim2div  27355  prodeq2ii  27377  fprodcvg  27394  prodmolem2a  27398  zprod  27401  fprodntriv  27406  fprodser  27413  fprodm1  27428  fprodp1  27430  fprodeq0  27437  preduz  27612  nn0prpwlem  28470  fdc  28594  mettrifi  28606  caushft  28610  rmspecsqrnq  29200  rmspecnonsq  29201  rmspecfund  29203  rmxyadd  29215  rmxy1  29216  rmxm1  29228  rmxluc  29230  rmyluc2  29232  jm2.17a  29256  jm2.18  29290  jm2.22  29297  jm2.15nn0  29305  jm2.16nn0  29306  jm2.27a  29307  jm2.27c  29309  jm3.1lem2  29320  jm3.1lem3  29321  jm3.1  29322  expdiophlem1  29323  fmul01  29714  fmul01lt1lem1  29718  fmul01lt1lem2  29719  climsuselem1  29733  climsuse  29734  itgsinexp  29748  fzisfzounsn  30164  eluzgtdifelfzo  30172  extwwlkfablem2  30624
  Copyright terms: Public domain W3C validator