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

Theorem eluzelz 11735
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 11731 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 1097 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030   class class class wbr 4685  cfv 5926  cle 10113  cz 11415  cuz 11725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-cnex 10030  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416  df-uz 11726
This theorem is referenced by:  eluzelre  11736  uztrn  11742  uzneg  11744  uzss  11746  eluzp1l  11750  eluzaddi  11752  eluzsubi  11753  uzm1  11756  uzin  11758  uzind4  11784  uzwo  11789  uz2mulcl  11804  uzsupss  11818  elfz5  12372  elfzel2  12378  elfzelz  12380  eluzfz2  12387  peano2fzr  12392  fzsplit2  12404  fzopth  12416  ssfzunsn  12425  fzsuc  12426  elfz1uz  12448  uzsplit  12450  uzdisj  12451  fzm1  12458  uznfz  12461  nn0disj  12494  preduz  12500  elfzo3  12525  fzoss2  12535  fzouzsplit  12542  fzoun  12544  eluzgtdifelfzo  12569  fzosplitsnm1  12582  fzofzp1b  12606  elfzonelfzo  12610  fzosplitsn  12616  fzisfzounsn  12620  fldiv4lem1div2uz2  12677  m1modge3gt1  12757  modaddmodup  12773  om2uzlti  12789  om2uzf1oi  12792  uzrdgxfr  12806  fzen2  12808  seqfveq2  12863  seqfeq2  12864  seqshft2  12867  monoord  12871  monoord2  12872  sermono  12873  seqsplit  12874  seqf1olem1  12880  seqf1olem2  12881  seqid  12886  seqz  12889  leexp2a  12956  expnlbnd2  13035  expmulnbnd  13036  hashfz  13252  fzsdom2  13253  hashfzo  13254  hashfzp1  13256  seqcoll  13286  swrdfv2  13492  swrdccatin12  13537  rexuz3  14132  r19.2uz  14135  rexuzre  14136  cau4  14140  caubnd2  14141  clim  14269  climrlim2  14322  climshft2  14357  climaddc1  14409  climmulc2  14411  climsubc1  14412  climsubc2  14413  clim2ser  14429  clim2ser2  14430  iserex  14431  climlec2  14433  climub  14436  isercolllem2  14440  isercoll  14442  isercoll2  14443  climcau  14445  caurcvg2  14452  caucvgb  14454  serf0  14455  iseraltlem1  14456  iseraltlem2  14457  iseralt  14459  sumrblem  14486  fsumcvg  14487  summolem2a  14490  fsumcvg2  14502  fsumm1  14524  fzosump1  14525  fsump1  14531  fsumrev2  14558  telfsumo  14578  fsumparts  14582  isumsplit  14616  isumrpcl  14619  isumsup2  14622  cvgrat  14659  mertenslem1  14660  clim2div  14665  prodeq2ii  14687  fprodcvg  14704  prodmolem2a  14708  zprod  14711  fprodntriv  14716  fprodser  14723  fprodm1  14741  fprodp1  14743  fprodeq0  14749  isprm3  15443  nprm  15448  dvdsprm  15462  exprmfct  15463  isprm5  15466  maxprmfct  15468  ncoprmlnprm  15483  phibndlem  15522  dfphi2  15526  hashdvds  15527  pcaddlem  15639  pcfac  15650  expnprm  15653  prmreclem4  15670  vdwlem8  15739  gsumval2a  17326  efgs1b  18195  telgsumfzs  18432  iscau4  23123  caucfil  23127  iscmet3lem3  23134  iscmet3lem1  23135  iscmet3lem2  23136  lmle  23145  uniioombllem3  23399  mbflimsup  23478  mbfi1fseqlem6  23532  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  aaliou3lem1  24142  aaliou3lem2  24143  ulmres  24187  ulmshftlem  24188  ulmshft  24189  ulmcaulem  24193  ulmcau  24194  ulmdvlem1  24199  radcnvlem1  24212  logblt  24567  muval1  24904  chtdif  24929  ppidif  24934  chtub  24982  bcmono  25047  bpos1lem  25052  lgsquad2lem2  25155  2sqlem6  25193  2sqlem8a  25195  2sqlem8  25196  chebbnd1lem1  25203  dchrisumlem2  25224  dchrisum0lem1  25250  ostthlem2  25362  ostth2  25371  axlowdimlem3  25869  axlowdimlem6  25872  axlowdimlem7  25873  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  extwwlkfablem  27326  2clwwlk2clwwlklem2lem1  27328  fzspl  29678  fzdif2  29679  supfz  31739  divcnvlin  31744  nn0prpwlem  32442  fdc  33671  mettrifi  33683  caushft  33687  rmspecnonsq  37789  rmspecfund  37791  rmxyadd  37803  rmxy1  37804  jm2.18  37872  jm2.22  37879  jm2.15nn0  37887  jm2.16nn0  37888  jm2.27a  37889  jm2.27c  37891  jm3.1lem2  37902  jm3.1lem3  37903  jm3.1  37904  expdiophlem1  37905  dvgrat  38828  cvgdvgrat  38829  hashnzfz  38836  uzwo4  39535  ssinc  39578  ssdec  39579  rexanuz3  39589  monoords  39825  fzdifsuc2  39838  iuneqfzuzlem  39863  eluzelzd  39904  allbutfi  39929  eluzelz2  39940  uzid2  39943  monoordxrv  40025  monoord2xrv  40027  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  climsuselem1  40157  climsuse  40158  climf  40172  climresmpt  40209  climf2  40216  limsupequzlem  40272  limsupmnfuzlem  40276  limsupre3uzlem  40285  itgsinexp  40488  iblspltprt  40507  itgspltprt  40513  iundjiunlem  40994  iundjiun  40995  smflimsuplem2  41348  smflimsuplem4  41350  smflimsuplem5  41351  fzopredsuc  41658  smonoord  41666  iccpartiltu  41683  pfxccatin12  41750  fmtnoprmfac2lem1  41803  fmtnofac2lem  41805  lighneallem2  41848  lighneallem4a  41850  lighneallem4b  41851  gboge9  41977  nnsum3primesle9  42007  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem2  42019  m1modmmod  42641  fllogbd  42679  fllog2  42687  dignn0ldlem  42721  dignnld  42722  digexp  42726  dignn0flhalf  42737  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator