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

Theorem eluzelz 11914
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 11910 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 1169 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156   class class class wbr 4844  cfv 6101  cle 10360  cz 11643  cuz 11904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-cnex 10277  ax-resscn 10278
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-ov 6877  df-neg 10554  df-z 11644  df-uz 11905
This theorem is referenced by:  eluzelre  11915  uztrn  11921  uzneg  11923  uzss  11925  eluzp1l  11929  eluzaddi  11931  eluzsubi  11932  subeluzsub  11935  uzm1  11936  uzin  11938  uzind4  11964  uzwo  11970  uz2mulcl  11985  uzsupss  11999  elfz5  12557  elfzel2  12563  elfzelz  12565  eluzfz2  12572  peano2fzr  12577  fzsplit2  12589  fzopth  12601  ssfzunsn  12610  fzsuc  12611  elfz1uz  12633  uzsplit  12635  uzdisj  12636  fzm1  12643  uznfz  12646  nn0disj  12679  preduz  12685  elfzo3  12710  fzoss2  12720  fzouzsplit  12727  fzoun  12729  eluzgtdifelfzo  12754  fzosplitsnm1  12767  fzofzp1b  12790  elfzonelfzo  12794  fzosplitsn  12800  fzisfzounsn  12804  fldiv4lem1div2uz2  12861  m1modge3gt1  12941  modaddmodup  12957  om2uzlti  12973  om2uzf1oi  12976  uzrdgxfr  12990  fzen2  12992  seqfveq2  13046  seqfeq2  13047  seqshft2  13050  monoord  13054  monoord2  13055  sermono  13056  seqsplit  13057  seqf1olem1  13063  seqf1olem2  13064  seqid  13069  seqz  13072  leexp2a  13139  expnlbnd2  13218  expmulnbnd  13219  hashfz  13431  fzsdom2  13432  hashfzo  13433  hashfzp1  13435  seqcoll  13465  swrdfv2  13670  swrdccatin12  13715  rexuz3  14311  r19.2uz  14314  rexuzre  14315  cau4  14319  caubnd2  14320  clim  14448  climrlim2  14501  climshft2  14536  climaddc1  14588  climmulc2  14590  climsubc1  14591  climsubc2  14592  clim2ser  14608  clim2ser2  14609  iserex  14610  climlec2  14612  climub  14615  isercolllem2  14619  isercoll  14621  isercoll2  14622  climcau  14624  caurcvg2  14631  caucvgb  14633  serf0  14634  iseraltlem1  14635  iseraltlem2  14636  iseralt  14638  sumrblem  14665  fsumcvg  14666  summolem2a  14669  fsumcvg2  14681  fsumm1  14703  fzosump1  14704  fsump1  14710  fsumrev2  14736  telfsumo  14756  fsumparts  14760  isumsplit  14794  isumrpcl  14797  isumsup2  14800  cvgrat  14836  mertenslem1  14837  clim2div  14842  prodeq2ii  14864  fprodcvg  14881  prodmolem2a  14885  zprod  14888  fprodntriv  14893  fprodser  14900  fprodm1  14918  fprodp1  14920  fprodeq0  14926  isprm3  15614  nprm  15619  dvdsprm  15632  exprmfct  15633  isprm5  15636  maxprmfct  15638  ncoprmlnprm  15653  phibndlem  15692  dfphi2  15696  hashdvds  15697  pcaddlem  15809  pcfac  15820  expnprm  15823  prmreclem4  15840  vdwlem8  15909  gsumval2a  17484  efgs1b  18350  telgsumfzs  18588  iscau4  23289  caucfil  23293  iscmet3lem3  23300  iscmet3lem1  23301  iscmet3lem2  23302  lmle  23311  uniioombllem3  23566  mbflimsup  23647  mbfi1fseqlem6  23701  dvfsumle  23998  dvfsumge  23999  dvfsumabs  24000  aaliou3lem1  24311  aaliou3lem2  24312  ulmres  24356  ulmshftlem  24357  ulmshft  24358  ulmcaulem  24362  ulmcau  24363  ulmdvlem1  24368  radcnvlem1  24381  logblt  24736  muval1  25073  chtdif  25098  ppidif  25103  chtub  25151  bcmono  25216  bpos1lem  25221  lgsquad2lem2  25324  2sqlem6  25362  2sqlem8a  25364  2sqlem8  25365  chebbnd1lem1  25372  dchrisumlem2  25393  dchrisum0lem1  25419  ostthlem2  25531  ostth2  25540  axlowdimlem3  26038  axlowdimlem6  26041  axlowdimlem7  26042  axlowdimlem16  26051  axlowdimlem17  26052  axlowdim  26055  clwwnrepclwwn  27521  fzspl  29877  fzdif2  29878  supfz  31935  divcnvlin  31940  nn0prpwlem  32638  fdc  33852  mettrifi  33864  caushft  33868  rmspecnonsq  37973  rmspecfund  37975  rmxyadd  37987  rmxy1  37988  jm2.18  38056  jm2.22  38063  jm2.15nn0  38071  jm2.16nn0  38072  jm2.27a  38073  jm2.27c  38075  jm3.1lem2  38086  jm3.1lem3  38087  jm3.1  38088  expdiophlem1  38089  dvgrat  39011  cvgdvgrat  39012  hashnzfz  39019  uzwo4  39714  ssinc  39757  ssdec  39758  rexanuz3  39768  monoords  39992  fzdifsuc2  40005  iuneqfzuzlem  40030  eluzelzd  40071  allbutfi  40095  eluzelz2  40106  uzid2  40109  monoordxrv  40191  monoord2xrv  40193  fmul01  40292  fmul01lt1lem1  40296  fmul01lt1lem2  40297  climsuselem1  40319  climsuse  40320  climf  40334  climresmpt  40371  climf2  40378  limsupequzlem  40434  limsupmnfuzlem  40438  limsupre3uzlem  40447  itgsinexp  40650  iblspltprt  40668  itgspltprt  40674  iundjiunlem  41155  iundjiun  41156  smflimsuplem2  41509  smflimsuplem4  41511  smflimsuplem5  41512  fzopredsuc  41908  smonoord  41916  iccpartiltu  41933  pfxccatin12  42000  fmtnoprmfac2lem1  42053  fmtnofac2lem  42055  lighneallem2  42098  lighneallem4a  42100  lighneallem4b  42101  gboge9  42227  nnsum3primesle9  42257  nnsum4primesevenALTV  42264  wtgoldbnnsum4prm  42265  bgoldbnnsum3prm  42267  bgoldbtbndlem2  42269  m1modmmod  42884  fllogbd  42922  fllog2  42930  dignn0ldlem  42964  dignnld  42965  digexp  42969  dignn0flhalf  42980  nn0sumshdiglemB  42982
  Copyright terms: Public domain W3C validator