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

Theorem eluzelz 11526
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 11522 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 1069 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   class class class wbr 4574  cfv 5787  cle 9928  cz 11207  cuz 11516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-cnex 9845  ax-resscn 9846
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-fv 5795  df-ov 6527  df-neg 10117  df-z 11208  df-uz 11517
This theorem is referenced by:  eluzelre  11527  uztrn  11533  uzneg  11535  uzss  11537  eluzp1l  11541  eluzaddi  11543  eluzsubi  11544  uzm1  11547  uzin  11549  uzind4  11575  uzwo  11580  uz2mulcl  11595  uzsupss  11609  elfz5  12157  elfzel2  12163  elfzelz  12165  eluzfz2  12172  peano2fzr  12177  fzsplit2  12189  fzopth  12201  ssfzunsn  12209  fzsuc  12210  uzsplit  12233  uzdisj  12234  fzm1  12241  uznfz  12244  nn0disj  12276  preduz  12282  elfzo3  12307  fzoss2  12317  fzouzsplit  12324  eluzgtdifelfzo  12349  fzosplitsnm1  12361  fzofzp1b  12384  elfzonelfzo  12388  fzosplitsn  12394  fzisfzounsn  12397  fldiv4lem1div2uz2  12451  m1modge3gt1  12531  modaddmodup  12547  om2uzlti  12563  om2uzf1oi  12566  uzrdgxfr  12580  fzen2  12582  seqfveq2  12637  seqfeq2  12638  seqshft2  12641  monoord  12645  monoord2  12646  sermono  12647  seqsplit  12648  seqf1olem1  12654  seqf1olem2  12655  seqid  12660  seqz  12663  leexp2a  12730  expnlbnd2  12809  expmulnbnd  12810  hashfz  13023  fzsdom2  13024  hashfzo  13025  hashfzp1  13027  seqcoll  13054  swrdfv2  13241  swrdccatin12  13285  rexuz3  13879  r19.2uz  13882  rexuzre  13883  cau4  13887  caubnd2  13888  clim  14016  climrlim2  14069  climshft2  14104  climaddc1  14156  climmulc2  14158  climsubc1  14159  climsubc2  14160  clim2ser  14176  clim2ser2  14177  iserex  14178  climlec2  14180  climub  14183  isercolllem2  14187  isercoll  14189  isercoll2  14190  climcau  14192  caurcvg2  14199  caucvgb  14201  serf0  14202  iseraltlem1  14203  iseraltlem2  14204  iseralt  14206  sumrblem  14232  fsumcvg  14233  summolem2a  14236  fsumcvg2  14248  fsumm1  14267  fzosump1  14268  fsump1  14272  fsumrev2  14299  telfsumo  14318  fsumparts  14322  isumsplit  14354  isumrpcl  14357  isumsup2  14360  cvgrat  14397  mertenslem1  14398  clim2div  14403  prodeq2ii  14425  fprodcvg  14442  prodmolem2a  14446  zprod  14449  fprodntriv  14454  fprodser  14461  fprodm1  14479  fprodp1  14481  fprodeq0  14487  isprm3  15177  nprm  15182  dvdsprm  15196  exprmfct  15197  isprm5  15200  maxprmfct  15202  ncoprmlnprm  15217  phibndlem  15256  dfphi2  15260  hashdvds  15261  pcaddlem  15373  pcfac  15384  expnprm  15387  prmreclem4  15404  vdwlem8  15473  gsumval2a  17045  efgs1b  17915  telgsumfzs  18152  iscau4  22800  caucfil  22804  iscmet3lem3  22811  iscmet3lem1  22812  iscmet3lem2  22813  lmle  22822  uniioombllem3  23073  mbflimsup  23153  mbfi1fseqlem6  23207  dvfsumle  23502  dvfsumge  23503  dvfsumabs  23504  aaliou3lem1  23815  aaliou3lem2  23816  ulmres  23860  ulmshftlem  23861  ulmshft  23862  ulmcaulem  23866  ulmcau  23867  ulmdvlem1  23872  radcnvlem1  23885  logblt  24236  muval1  24573  chtdif  24598  ppidif  24603  chtub  24651  bcmono  24716  bpos1lem  24721  lgsquad2lem2  24824  2sqlem6  24862  2sqlem8a  24864  2sqlem8  24865  chebbnd1lem1  24872  dchrisumlem2  24893  dchrisum0lem1  24919  ostthlem2  25031  ostth2  25040  axlowdimlem3  25539  axlowdimlem6  25542  axlowdimlem7  25543  axlowdimlem16  25552  axlowdimlem17  25553  axlowdim  25556  constr3trllem3  25943  extwwlkfablem2  26368  fzspl  28741  fzdif2  28742  supfz  30669  divcnvlin  30674  nn0prpwlem  31290  fdc  32511  mettrifi  32523  caushft  32527  rmspecnonsq  36290  rmspecfund  36292  rmxyadd  36304  rmxy1  36305  jm2.18  36373  jm2.22  36380  jm2.15nn0  36388  jm2.16nn0  36389  jm2.27a  36390  jm2.27c  36392  jm3.1lem2  36403  jm3.1lem3  36404  jm3.1  36405  expdiophlem1  36406  dvgrat  37333  cvgdvgrat  37334  hashnzfz  37341  uzwo4  38046  ssinc  38092  ssdec  38093  rexanuz3  38103  monoords  38252  fzdifsuc2  38267  iuneqfzuzlem  38292  eluzelzd  38333  allbutfi  38358  fmul01  38448  fmul01lt1lem1  38452  fmul01lt1lem2  38453  climsuselem1  38475  climsuse  38476  climf  38490  climresmpt  38527  climf2  38534  itgsinexp  38647  iblspltprt  38666  itgspltprt  38672  iundjiunlem  39153  iundjiun  39154  smonoord  39746  fzopredsuc  39748  iccpartiltu  39762  fmtnoprmfac2lem1  39818  fmtnofac2lem  39820  lighneallem2  39863  lighneallem4a  39865  lighneallem4b  39866  gboage9  39988  nnsum3primesle9  40012  nnsum4primesevenALTV  40019  wtgoldbnnsum4prm  40020  bgoldbnnsum3prm  40022  bgoldbtbndlem2  40024  pfxccatin12  40090  av-extwwlkfablem2  41509  m1modmmod  42109  fllogbd  42151  fllog2  42159  dignn0ldlem  42193  dignnld  42194  digexp  42198  dignn0flhalf  42209  nn0sumshdiglemB  42211
  Copyright terms: Public domain W3C validator