Theorem eluzfz2 13193

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

Step	Hyp	Ref	Expression
1		eluzelz 12521	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12526	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13180	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 683	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  ℤcz 12249  ℤ_≥cuz 12511  ...cfz 13168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-pre-lttri 10876

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-neg 11138  df-z 12250  df-uz 12512  df-fz 13169

This theorem is referenced by:  eluzfz2b  13194  elfzubelfz  13197  fzopth  13222  fzsuc  13232  fseq1p1m1  13259  fzm1  13265  fzneuz  13266  fzoend  13406  uzindi  13630  seqcl2  13669  seqfveq2  13673  seqshft2  13677  monoord  13681  monoord2  13682  seqsplit  13684  seqcaopr3  13686  seqf1olem2a  13689  seqf1olem1  13690  seqf1olem2  13691  seqid2  13697  seqhomo  13698  seqcoll  14106  seqcoll2  14107  wrdeqs1cat  14361  pfxccatin12lem2  14372  pfxccatin12lem3  14373  splid  14394  spllen  14395  splval2  14398  summolem2a  15355  fsumm1  15391  telfsumo  15442  telfsumo2  15443  fsumparts  15446  prodfn0  15534  prodfrec  15535  prodmolem2a  15572  fprodm1  15605  sadadd  16102  sadass  16106  smuval2  16117  vdwlem6  16615  efgredleme  19264  efgredlemc  19266  efgcpbllemb  19276  frgpuplem  19293  telgsumfzslem  19504  telgsumfzs  19505  pmatcollpw3fi1lem1  21843  chfacfisf  21911  chfacfisfcpmat  21912  iscmet3lem1  24360  iscmet3lem2  24361  voliunlem1  24619  volsup  24625  mbfi1fseqlem3  24787  wilthlem2  26123  wilthlem3  26124  chtub  26265  dchrisum0flb  26563  pntpbnd1  26639  pntlemf  26658  spthonepeq  28021  wwlksnext  28159  2clwwlk2clwwlklem  28611  clwwlknonclwlknonf1o  28627  wrdsplex  31114  cycpmco2f1  31293  submatres  31658  madjusmdetlem1  31679  madjusmdetlem2  31680  madjusmdetlem3  31681  madjusmdetlem4  31682  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemfrci  32394  gsumnunsn  32420  swrdrevpfx  32978  cvmliftlem10  33156  supfz  33600  fwddifnp1  34394  poimirlem3  35707  poimirlem4  35708  poimirlem16  35720  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem31  35735  volsupnfl  35749  sdclem2  35827  fdc  35830  mettrifi  35842  iunincfi  42533  monoordxrv  42912  monoord2xrv  42914  fmul01lt1lem2  43016  limsupubuzlem  43143  dvnmul  43374  dvnprodlem3  43379  stoweidlem3  43434  stoweidlem11  43442  stoweidlem17  43448  stoweidlem34  43465  fourierdlem15  43553  fourierdlem25  43563  fourierdlem50  43587  fourierdlem52  43589  fourierdlem54  43591  fourierdlem65  43602  fourierdlem81  43618  fourierdlem92  43629  fourierdlem102  43639  fourierdlem111  43648  fourierdlem113  43650  fourierdlem114  43651  etransclem35  43700  sge0p1  43842  carageniuncllem1  43949  caratheodorylem1  43954  smfmullem4  44215  ssfz12  44694  elfzlble  44700  smonoord  44711