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

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

Proof of Theorem eluzfz2
StepHypRef Expression
1 eluzelz 12241 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
2 uzid 12246 . . 3 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
31, 2syl 17 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (ℤ𝑁))
4 eluzfz 12891 . 2 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑁)) → 𝑁 ∈ (𝑀...𝑁))
53, 4mpdan 683 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cfv 6348  (class class class)co 7145  cz 11969  cuz 12231  ...cfz 12880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-pre-lttri 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7678  df-2nd 7679  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-neg 10861  df-z 11970  df-uz 12232  df-fz 12881
This theorem is referenced by:  eluzfz2b  12904  elfzubelfz  12907  fzopth  12932  fzsuc  12942  fseq1p1m1  12969  fzm1  12975  fzneuz  12976  fzoend  13116  uzindi  13338  seqcl2  13376  seqfveq2  13380  seqshft2  13384  monoord  13388  monoord2  13389  seqsplit  13391  seqcaopr3  13393  seqf1olem2a  13396  seqf1olem1  13397  seqf1olem2  13398  seqid2  13404  seqhomo  13405  seqcoll  13810  seqcoll2  13811  wrdeqs1cat  14070  pfxccatin12lem2  14081  pfxccatin12lem3  14082  splid  14103  spllen  14104  splval2  14107  summolem2a  15060  fsumm1  15094  telfsumo  15145  telfsumo2  15146  fsumparts  15149  prodfn0  15238  prodfrec  15239  prodmolem2a  15276  fprodm1  15309  sadadd  15804  sadass  15808  smuval2  15819  vdwlem6  16310  efgredleme  18798  efgredlemc  18800  efgcpbllemb  18810  frgpuplem  18827  telgsumfzslem  19037  telgsumfzs  19038  pmatcollpw3fi1lem1  21322  chfacfisf  21390  chfacfisfcpmat  21391  iscmet3lem1  23821  iscmet3lem2  23822  voliunlem1  24078  volsup  24084  mbfi1fseqlem3  24245  wilthlem2  25573  wilthlem3  25574  chtub  25715  dchrisum0flb  26013  pntpbnd1  26089  pntlemf  26108  spthonepeq  27460  wwlksnext  27598  2clwwlk2clwwlklem  28052  clwwlknonclwlknonf1o  28068  wrdsplex  30541  cycpmco2f1  30693  submatres  30970  madjusmdetlem1  30991  madjusmdetlem2  30992  madjusmdetlem3  30993  madjusmdetlem4  30994  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemfrci  31684  gsumnunsn  31710  swrdrevpfx  32260  cvmliftlem10  32438  supfz  32857  fwddifnp1  33523  poimirlem3  34776  poimirlem4  34777  poimirlem16  34789  poimirlem19  34792  poimirlem20  34793  poimirlem23  34796  poimirlem31  34804  volsupnfl  34818  sdclem2  34898  fdc  34901  mettrifi  34913  iunincfi  41237  monoordxrv  41634  monoord2xrv  41636  fmul01lt1lem2  41742  limsupubuzlem  41869  dvnmul  42104  dvnprodlem3  42109  stoweidlem3  42165  stoweidlem11  42173  stoweidlem17  42179  stoweidlem34  42196  fourierdlem15  42284  fourierdlem25  42294  fourierdlem50  42318  fourierdlem52  42320  fourierdlem54  42322  fourierdlem65  42333  fourierdlem81  42349  fourierdlem92  42360  fourierdlem102  42370  fourierdlem111  42379  fourierdlem113  42381  fourierdlem114  42382  etransclem35  42431  sge0p1  42573  carageniuncllem1  42680  caratheodorylem1  42685  smfmullem4  42946  ssfz12  43391  elfzlble  43397  smonoord  43408
  Copyright terms: Public domain W3C validator