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

Theorem eluzelz 12774
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 12770 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 1147 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106  cfv 6497  cle 11191  cz 12500  cuz 12764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-cnex 11108  ax-resscn 11109
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505  df-ov 7361  df-neg 11389  df-z 12501  df-uz 12765
This theorem is referenced by:  eluzelre  12775  uztrn  12782  uzneg  12784  uzss  12787  eluzp1l  12791  eluzadd  12793  eluzsub  12794  eluzaddiOLD  12796  eluzsubiOLD  12798  subeluzsub  12801  uzm1  12802  uzin  12804  uzind4  12832  uzwo  12837  uz2mulcl  12852  uzsupss  12866  elfz5  13434  elfzel2  13440  elfzelz  13442  eluzfz2  13450  peano2fzr  13455  fzsplit2  13467  fzopth  13479  ssfzunsn  13488  fzsuc  13489  elfz1uz  13512  uzsplit  13514  uzdisj  13515  fzm1  13522  uznfz  13525  nn0disj  13558  preduz  13564  elfzo3  13590  fzoss2  13601  fzouzsplit  13608  fzoun  13610  eluzgtdifelfzo  13635  fzosplitsnm1  13648  fzofzp1b  13671  elfzonelfzo  13675  fzosplitsn  13681  fzisfzounsn  13685  fldiv4lem1div2uz2  13742  m1modge3gt1  13824  modaddmodup  13840  om2uzlti  13856  om2uzf1oi  13859  uzrdgxfr  13873  fzen2  13875  seqfveq2  13931  seqfeq2  13932  seqshft2  13935  monoord  13939  monoord2  13940  sermono  13941  seqsplit  13942  seqf1olem1  13948  seqf1olem2  13949  seqid  13954  leexp2a  14078  expnlbnd2  14138  expmulnbnd  14139  hashfz  14328  fzsdom2  14329  hashfzo  14330  hashfzp1  14332  seqcoll  14364  swrdfv2  14550  pfxccatin12  14622  rexuz3  15234  r19.2uz  15237  rexuzre  15238  cau4  15242  caubnd2  15243  clim  15377  climrlim2  15430  climshft2  15465  climaddc1  15518  climmulc2  15520  climsubc1  15521  climsubc2  15522  clim2ser  15540  clim2ser2  15541  iserex  15542  climlec2  15544  climub  15547  isercolllem2  15551  isercoll  15553  isercoll2  15554  climcau  15556  caurcvg2  15563  caucvgb  15565  serf0  15566  iseraltlem1  15567  iseraltlem2  15568  iseralt  15570  sumrblem  15597  fsumcvg  15598  summolem2a  15601  fsumcvg2  15613  fsumm1  15637  fzosump1  15638  fsump1  15642  fsumrev2  15668  telfsumo  15688  fsumparts  15692  isumsplit  15726  isumrpcl  15729  isumsup2  15732  cvgrat  15769  mertenslem1  15770  clim2div  15775  prodeq2ii  15797  fprodcvg  15814  prodmolem2a  15818  zprod  15821  fprodntriv  15826  fprodser  15833  fprodm1  15851  fprodp1  15853  fprodeq0  15859  isprm3  16560  nprm  16565  dvdsprm  16580  exprmfct  16581  isprm5  16584  maxprmfct  16586  prmdvdsncoprmbd  16603  ncoprmlnprm  16604  phibndlem  16643  dfphi2  16647  hashdvds  16648  pcaddlem  16761  pcfac  16772  expnprm  16775  prmreclem4  16792  vdwlem8  16861  gsumval2a  18541  efgs1b  19519  telgsumfzs  19767  iscau4  24646  caucfil  24650  iscmet3lem3  24657  iscmet3lem1  24658  iscmet3lem2  24659  lmle  24668  uniioombllem3  24952  mbflimsup  25033  mbfi1fseqlem6  25088  dvfsumle  25388  dvfsumge  25389  dvfsumabs  25390  aaliou3lem1  25705  aaliou3lem2  25706  ulmres  25750  ulmshftlem  25751  ulmshft  25752  ulmcaulem  25756  ulmcau  25757  ulmdvlem1  25762  radcnvlem1  25775  logblt  26137  logbgcd1irr  26147  muval1  26485  chtdif  26510  ppidif  26515  chtub  26563  bcmono  26628  bpos1lem  26633  lgsquad2lem2  26736  2sqlem6  26774  2sqlem8a  26776  2sqlem8  26777  chebbnd1lem1  26820  dchrisumlem2  26841  dchrisum0lem1  26867  ostthlem2  26979  ostth2  26988  axlowdimlem3  27896  axlowdimlem6  27899  axlowdimlem7  27900  axlowdimlem16  27909  axlowdimlem17  27910  axlowdim  27913  clwwnrepclwwn  29291  fzspl  31696  fzdif2  31697  supfz  34304  divcnvlin  34308  nn0prpwlem  34797  fdc  36207  mettrifi  36219  caushft  36223  aks4d1lem1  40522  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p5  40540  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8  40547  aks4d1p9  40548  fzosumm1  40670  dffltz  40975  rmspecnonsq  41233  rmspecfund  41235  rmxyadd  41248  rmxy1  41249  jm2.18  41315  jm2.22  41322  jm2.15nn0  41330  jm2.16nn0  41331  jm2.27a  41332  jm2.27c  41334  jm3.1lem2  41345  jm3.1lem3  41346  jm3.1  41347  expdiophlem1  41348  dvgrat  42599  cvgdvgrat  42600  hashnzfz  42607  uzwo4  43268  ssinc  43304  ssdec  43305  rexanuz3  43313  monoords  43538  fzdifsuc2  43551  iuneqfzuzlem  43575  eluzelzd  43616  allbutfi  43635  eluzelz2  43645  uzid2  43647  monoordxrv  43724  monoord2xrv  43726  fmul01  43828  fmul01lt1lem1  43832  fmul01lt1lem2  43833  climsuselem1  43855  climsuse  43856  climf  43870  climresmpt  43907  climf2  43914  limsupequzlem  43970  limsupmnfuzlem  43974  limsupre3uzlem  43983  itgsinexp  44203  iblspltprt  44221  itgspltprt  44227  iundjiun  44708  smflimsuplem2  45069  smflimsuplem4  45071  smflimsuplem5  45072  fzopredsuc  45562  smonoord  45570  iccpartiltu  45621  fmtnoprmfac2lem1  45765  fmtnofac2lem  45767  lighneallem2  45805  lighneallem4a  45807  lighneallem4b  45808  fppr2odd  45930  fpprwpprb  45939  gboge9  45963  nnsum3primesle9  45993  nnsum4primesevenALTV  46000  wtgoldbnnsum4prm  46001  bgoldbnnsum3prm  46003  bgoldbtbndlem2  46005  m1modmmod  46614  fllogbd  46653  fllog2  46661  dignn0ldlem  46695  dignnld  46696  digexp  46700  dignn0flhalf  46711  nn0sumshdiglemB  46713
  Copyright terms: Public domain W3C validator