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

Theorem eluzfz1 12897
Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
eluzfz1 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))

Proof of Theorem eluzfz1
StepHypRef Expression
1 eluzel2 12226 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 uzid 12236 . . 3 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
31, 2syl 17 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (ℤ𝑀))
4 eluzfz 12886 . 2 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑀 ∈ (𝑀...𝑁))
53, 4mpancom 687 1 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  cfv 6328  (class class class)co 7130  cz 11959  cuz 12221  ...cfz 12875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-pre-lttri 10588
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7133  df-oprab 7134  df-mpo 7135  df-1st 7664  df-2nd 7665  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-neg 10850  df-z 11960  df-uz 12222  df-fz 12876
This theorem is referenced by:  elfz3  12900  fzn0  12904  fzopth  12927  seqcl  13374  seqfveq  13378  seqshft2  13380  monoord  13384  monoord2  13385  seqcaopr3  13389  seqf1olem2a  13392  seqf1olem2  13394  seqhomo  13401  seqcoll  13806  fsum1p  15087  telfsumo  15136  telfsumo2  15137  fsumparts  15140  mertenslem2  15220  prodfn0  15229  prodfrec  15230  fprod1p  15301  phicl2  16082  eulerthlem2  16096  4sqlem19  16276  vdwlem1  16294  vdwlem6  16299  vdw  16307  fvprmselelfz  16357  prmodvdslcmf  16360  gsumval2  17875  gsumsplit1r  17876  efgsdmi  18837  gsumval3  19006  telgsumfzslem  19087  telgsumfzs  19088  pmatcollpw3fi1lem1  21370  chfacfisf  21438  chfacfisfcpmat  21439  cpmadugsumlemF  21460  imasdsf1olem  22959  ovoliunlem1  24085  mbfi1fseqlem3  24300  cxpeq  25325  ppiltx  25741  logexprlim  25788  dchrmusum2  26057  dchrvmasum2lem  26059  mudivsum  26093  mulogsum  26095  mulog2sumlem2  26098  axlowdimlem13  26727  axlowdim1  26732  axlowdim  26734  crctcshwlkn0lem6  27580  fzto1stfv1  30751  fzto1stinvn  30754  cycpmco2f1  30774  lmatfval  31090  lmat22e11  31094  ballotlem4  31764  ballotlemic  31772  ballotlem1c  31773  ballotlem1ri  31800  subfacp1lem1  32434  subfacp1lem5  32439  subfacp1lem6  32440  cvmliftlem10  32549  cvmliftlem13  32551  inffz  32969  fwddifnp1  33634  poimirlem6  34949  poimirlem7  34950  poimirlem16  34959  poimirlem17  34960  poimirlem19  34962  poimirlem28  34971  fdc  35069  mettrifi  35081  monoordxrv  41944  monoord2xrv  41946  fmul01lt1lem1  42049  dvnmptdivc  42403  dvnmul  42408  itgspltprt  42444  stoweidlem17  42482  stoweidlem20  42485  stoweidlem34  42499  fourierdlem15  42587  fourierdlem48  42619  fourierdlem50  42621  fourierdlem52  42623  fourierdlem54  42625  fourierdlem64  42635  fourierdlem81  42652  fourierdlem102  42673  fourierdlem103  42674  fourierdlem104  42675  fourierdlem111  42682  fourierdlem114  42685  etransclem10  42709  etransclem14  42713  etransclem15  42714  etransclem24  42723  etransclem35  42734  etransclem44  42743  smfmullem4  43249  ssfz12  43694  smonoord  43711
  Copyright terms: Public domain W3C validator