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

Theorem eluzelz 11682
Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
eluzelz (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)

Proof of Theorem eluzelz
StepHypRef Expression
1 eluz2 11678 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 1075 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988   class class class wbr 4644  cfv 5876  cle 10060  cz 11362  cuz 11672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-cnex 9977  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-ov 6638  df-neg 10254  df-z 11363  df-uz 11673
This theorem is referenced by:  eluzelre  11683  uztrn  11689  uzneg  11691  uzss  11693  eluzp1l  11697  eluzaddi  11699  eluzsubi  11700  uzm1  11703  uzin  11705  uzind4  11731  uzwo  11736  uz2mulcl  11751  uzsupss  11765  elfz5  12319  elfzel2  12325  elfzelz  12327  eluzfz2  12334  peano2fzr  12339  fzsplit2  12351  fzopth  12363  ssfzunsn  12372  fzsuc  12373  uzsplit  12396  uzdisj  12397  fzm1  12404  uznfz  12407  nn0disj  12439  preduz  12445  elfzo3  12470  fzoss2  12480  fzouzsplit  12487  eluzgtdifelfzo  12513  fzosplitsnm1  12526  fzofzp1b  12550  elfzonelfzo  12554  fzosplitsn  12560  fzisfzounsn  12563  fldiv4lem1div2uz2  12620  m1modge3gt1  12700  modaddmodup  12716  om2uzlti  12732  om2uzf1oi  12735  uzrdgxfr  12749  fzen2  12751  seqfveq2  12806  seqfeq2  12807  seqshft2  12810  monoord  12814  monoord2  12815  sermono  12816  seqsplit  12817  seqf1olem1  12823  seqf1olem2  12824  seqid  12829  seqz  12832  leexp2a  12899  expnlbnd2  12978  expmulnbnd  12979  hashfz  13197  fzsdom2  13198  hashfzo  13199  hashfzp1  13201  seqcoll  13231  swrdfv2  13428  swrdccatin12  13472  rexuz3  14069  r19.2uz  14072  rexuzre  14073  cau4  14077  caubnd2  14078  clim  14206  climrlim2  14259  climshft2  14294  climaddc1  14346  climmulc2  14348  climsubc1  14349  climsubc2  14350  clim2ser  14366  clim2ser2  14367  iserex  14368  climlec2  14370  climub  14373  isercolllem2  14377  isercoll  14379  isercoll2  14380  climcau  14382  caurcvg2  14389  caucvgb  14391  serf0  14392  iseraltlem1  14393  iseraltlem2  14394  iseralt  14396  sumrblem  14423  fsumcvg  14424  summolem2a  14427  fsumcvg2  14439  fsumm1  14461  fzosump1  14462  fsump1  14468  fsumrev2  14495  telfsumo  14515  fsumparts  14519  isumsplit  14553  isumrpcl  14556  isumsup2  14559  cvgrat  14596  mertenslem1  14597  clim2div  14602  prodeq2ii  14624  fprodcvg  14641  prodmolem2a  14645  zprod  14648  fprodntriv  14653  fprodser  14660  fprodm1  14678  fprodp1  14680  fprodeq0  14686  isprm3  15377  nprm  15382  dvdsprm  15396  exprmfct  15397  isprm5  15400  maxprmfct  15402  ncoprmlnprm  15417  phibndlem  15456  dfphi2  15460  hashdvds  15461  pcaddlem  15573  pcfac  15584  expnprm  15587  prmreclem4  15604  vdwlem8  15673  gsumval2a  17260  efgs1b  18130  telgsumfzs  18367  iscau4  23058  caucfil  23062  iscmet3lem3  23069  iscmet3lem1  23070  iscmet3lem2  23071  lmle  23080  uniioombllem3  23334  mbflimsup  23414  mbfi1fseqlem6  23468  dvfsumle  23765  dvfsumge  23766  dvfsumabs  23767  aaliou3lem1  24078  aaliou3lem2  24079  ulmres  24123  ulmshftlem  24124  ulmshft  24125  ulmcaulem  24129  ulmcau  24130  ulmdvlem1  24135  radcnvlem1  24148  logblt  24503  muval1  24840  chtdif  24865  ppidif  24870  chtub  24918  bcmono  24983  bpos1lem  24988  lgsquad2lem2  25091  2sqlem6  25129  2sqlem8a  25131  2sqlem8  25132  chebbnd1lem1  25139  dchrisumlem2  25160  dchrisum0lem1  25186  ostthlem2  25298  ostth2  25307  axlowdimlem3  25805  axlowdimlem6  25808  axlowdimlem7  25809  axlowdimlem16  25818  axlowdimlem17  25819  axlowdim  25822  extwwlkfablem2  27184  fzspl  29524  fzdif2  29525  supfz  31588  divcnvlin  31593  nn0prpwlem  32292  fdc  33512  mettrifi  33524  caushft  33528  rmspecnonsq  37291  rmspecfund  37293  rmxyadd  37305  rmxy1  37306  jm2.18  37374  jm2.22  37381  jm2.15nn0  37389  jm2.16nn0  37390  jm2.27a  37391  jm2.27c  37393  jm3.1lem2  37404  jm3.1lem3  37405  jm3.1  37406  expdiophlem1  37407  dvgrat  38331  cvgdvgrat  38332  hashnzfz  38339  uzwo4  39041  ssinc  39084  ssdec  39085  rexanuz3  39095  monoords  39324  fzdifsuc2  39338  iuneqfzuzlem  39363  eluzelzd  39404  allbutfi  39429  eluzelz2  39440  uzid2  39443  fmul01  39612  fmul01lt1lem1  39616  fmul01lt1lem2  39617  climsuselem1  39639  climsuse  39640  climf  39654  climresmpt  39691  climf2  39698  limsupequzlem  39754  limsupmnfuzlem  39758  limsupre3uzlem  39767  itgsinexp  39933  iblspltprt  39952  itgspltprt  39958  iundjiunlem  40439  iundjiun  40440  smflimsuplem2  40790  smflimsuplem4  40792  smflimsuplem5  40793  fzopredsuc  41096  smonoord  41105  iccpartiltu  41122  pfxccatin12  41190  fmtnoprmfac2lem1  41243  fmtnofac2lem  41245  lighneallem2  41288  lighneallem4a  41290  lighneallem4b  41291  gboge9  41417  nnsum3primesle9  41447  nnsum4primesevenALTV  41454  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  bgoldbtbndlem2  41459  m1modmmod  42081  fllogbd  42119  fllog2  42127  dignn0ldlem  42161  dignnld  42162  digexp  42166  dignn0flhalf  42177  nn0sumshdiglemB  42179
  Copyright terms: Public domain W3C validator