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

Theorem eluzelz 12247
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 12243 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 1140 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5063  cfv 6354  cle 10670  cz 11975  cuz 12237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-cnex 10587  ax-resscn 10588
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-fv 6362  df-ov 7153  df-neg 10867  df-z 11976  df-uz 12238
This theorem is referenced by:  eluzelre  12248  uztrn  12255  uzneg  12257  uzss  12259  eluzp1l  12263  eluzaddi  12265  eluzsubi  12266  subeluzsub  12269  uzm1  12270  uzin  12272  uzind4  12300  uzwo  12305  uz2mulcl  12320  uzsupss  12334  elfz5  12895  elfzel2  12901  elfzelz  12903  eluzfz2  12910  peano2fzr  12915  fzsplit2  12927  fzopth  12939  ssfzunsn  12948  fzsuc  12949  elfz1uz  12972  uzsplit  12974  uzdisj  12975  fzm1  12982  uznfz  12985  nn0disj  13018  preduz  13024  elfzo3  13049  fzoss2  13060  fzouzsplit  13067  fzoun  13069  eluzgtdifelfzo  13094  fzosplitsnm1  13107  fzofzp1b  13130  elfzonelfzo  13134  fzosplitsn  13140  fzisfzounsn  13144  fldiv4lem1div2uz2  13201  m1modge3gt1  13281  modaddmodup  13297  om2uzlti  13313  om2uzf1oi  13316  uzrdgxfr  13330  fzen2  13332  seqfveq2  13387  seqfeq2  13388  seqshft2  13391  monoord  13395  monoord2  13396  sermono  13397  seqsplit  13398  seqf1olem1  13404  seqf1olem2  13405  seqid  13410  seqz  13413  leexp2a  13531  expnlbnd2  13590  expmulnbnd  13591  hashfz  13783  fzsdom2  13784  hashfzo  13785  hashfzp1  13787  seqcoll  13817  swrdfv2  14018  pfxccatin12  14090  rexuz3  14703  r19.2uz  14706  rexuzre  14707  cau4  14711  caubnd2  14712  clim  14846  climrlim2  14899  climshft2  14934  climaddc1  14986  climmulc2  14988  climsubc1  14989  climsubc2  14990  clim2ser  15006  clim2ser2  15007  iserex  15008  climlec2  15010  climub  15013  isercolllem2  15017  isercoll  15019  isercoll2  15020  climcau  15022  caurcvg2  15029  caucvgb  15031  serf0  15032  iseraltlem1  15033  iseraltlem2  15034  iseralt  15036  sumrblem  15063  fsumcvg  15064  summolem2a  15067  fsumcvg2  15079  fsumm1  15101  fzosump1  15102  fsump1  15106  fsumrev2  15132  telfsumo  15152  fsumparts  15156  isumsplit  15190  isumrpcl  15193  isumsup2  15196  cvgrat  15234  mertenslem1  15235  clim2div  15240  prodeq2ii  15262  fprodcvg  15279  prodmolem2a  15283  zprod  15286  fprodntriv  15291  fprodser  15298  fprodm1  15316  fprodp1  15318  fprodeq0  15324  isprm3  16022  nprm  16027  dvdsprm  16042  exprmfct  16043  isprm5  16046  maxprmfct  16048  ncoprmlnprm  16063  phibndlem  16102  dfphi2  16106  hashdvds  16107  pcaddlem  16219  pcfac  16230  expnprm  16233  prmreclem4  16250  vdwlem8  16319  gsumval2a  17890  efgs1b  18798  telgsumfzs  19045  iscau4  23816  caucfil  23820  iscmet3lem3  23827  iscmet3lem1  23828  iscmet3lem2  23829  lmle  23838  uniioombllem3  24120  mbflimsup  24201  mbfi1fseqlem6  24255  dvfsumle  24552  dvfsumge  24553  dvfsumabs  24554  aaliou3lem1  24865  aaliou3lem2  24866  ulmres  24910  ulmshftlem  24911  ulmshft  24912  ulmcaulem  24916  ulmcau  24917  ulmdvlem1  24922  radcnvlem1  24935  logblt  25294  logbgcd1irr  25304  muval1  25643  chtdif  25668  ppidif  25673  chtub  25721  bcmono  25786  bpos1lem  25791  lgsquad2lem2  25894  2sqlem6  25932  2sqlem8a  25934  2sqlem8  25935  chebbnd1lem1  25978  dchrisumlem2  25999  dchrisum0lem1  26025  ostthlem2  26137  ostth2  26146  axlowdimlem3  26663  axlowdimlem6  26666  axlowdimlem7  26667  axlowdimlem16  26676  axlowdimlem17  26677  axlowdim  26680  clwwnrepclwwn  28056  fzspl  30445  fzdif2  30446  supfz  32863  divcnvlin  32867  nn0prpwlem  33573  fdc  34907  mettrifi  34919  caushft  34923  fzosumm1  39010  dffltz  39155  fltne  39156  rmspecnonsq  39388  rmspecfund  39390  rmxyadd  39402  rmxy1  39403  jm2.18  39469  jm2.22  39476  jm2.15nn0  39484  jm2.16nn0  39485  jm2.27a  39486  jm2.27c  39488  jm3.1lem2  39499  jm3.1lem3  39500  jm3.1  39501  expdiophlem1  39502  dvgrat  40528  cvgdvgrat  40529  hashnzfz  40536  uzwo4  41199  ssinc  41237  ssdec  41238  rexanuz3  41246  monoords  41448  fzdifsuc2  41461  iuneqfzuzlem  41486  eluzelzd  41527  allbutfi  41549  eluzelz2  41560  uzid2  41562  monoordxrv  41642  monoord2xrv  41644  fmul01  41745  fmul01lt1lem1  41749  fmul01lt1lem2  41750  climsuselem1  41772  climsuse  41773  climf  41787  climresmpt  41824  climf2  41831  limsupequzlem  41887  limsupmnfuzlem  41891  limsupre3uzlem  41900  itgsinexp  42124  iblspltprt  42142  itgspltprt  42148  iundjiunlem  42626  iundjiun  42627  smflimsuplem2  42980  smflimsuplem4  42982  smflimsuplem5  42983  fzopredsuc  43408  smonoord  43416  iccpartiltu  43433  fmtnoprmfac2lem1  43579  fmtnofac2lem  43581  lighneallem2  43622  lighneallem4a  43624  lighneallem4b  43625  fppr2odd  43747  fpprwpprb  43756  gboge9  43780  nnsum3primesle9  43810  nnsum4primesevenALTV  43817  wtgoldbnnsum4prm  43818  bgoldbnnsum3prm  43820  bgoldbtbndlem2  43822  m1modmmod  44483  fllogbd  44522  fllog2  44530  dignn0ldlem  44564  dignnld  44565  digexp  44569  dignn0flhalf  44580  nn0sumshdiglemB  44582
  Copyright terms: Public domain W3C validator