Theorem eluzfz2 13450

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 12763	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12768	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13437	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 688	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6491  (class class class)co 7358  ℤcz 12490  ℤ_≥cuz 12753  ...cfz 13425

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085  ax-pre-lttri 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-neg 11369  df-z 12491  df-uz 12754  df-fz 13426

This theorem is referenced by:  eluzfz2b  13451  elfzubelfz  13454  fzopth  13479  fzsuc  13489  fseq1p1m1  13516  fzm1  13525  fzneuz  13526  fzoend  13675  uzindi  13907  seqcl2  13945  seqfveq2  13949  seqshft2  13953  monoord  13957  monoord2  13958  seqsplit  13960  seqcaopr3  13962  seqf1olem2a  13965  seqf1olem1  13966  seqf1olem2  13967  seqid2  13973  seqhomo  13974  seqcoll  14389  seqcoll2  14390  wrdeqs1cat  14645  pfxccatin12lem2  14656  pfxccatin12lem3  14657  splid  14678  spllen  14679  splval2  14682  summolem2a  15640  fsumm1  15676  telfsumo  15727  telfsumo2  15728  fsumparts  15731  prodfn0  15819  prodfrec  15820  prodmolem2a  15859  fprodm1  15892  sadadd  16396  sadass  16400  smuval2  16411  vdwlem6  16916  efgredleme  19674  efgredlemc  19676  efgcpbllemb  19686  frgpuplem  19703  telgsumfzslem  19919  telgsumfzs  19920  pmatcollpw3fi1lem1  22732  chfacfisf  22800  chfacfisfcpmat  22801  iscmet3lem1  25249  iscmet3lem2  25250  voliunlem1  25509  volsup  25515  mbfi1fseqlem3  25676  wilthlem2  27037  wilthlem3  27038  chtub  27181  dchrisum0flb  27479  pntpbnd1  27555  pntlemf  27574  spthonepeq  29806  wwlksnext  29947  2clwwlk2clwwlklem  30402  clwwlknonclwlknonf1o  30418  wrdsplex  32997  gsummptfzsplitra  33120  cycpmco2f1  33185  submatres  33942  madjusmdetlem1  33963  madjusmdetlem2  33964  madjusmdetlem3  33965  madjusmdetlem4  33966  ballotlemfc0  34629  ballotlemfcc  34630  ballotlemfrci  34664  gsumnunsn  34677  swrdrevpfx  35290  cvmliftlem10  35467  supfz  35902  fwddifnp1  36338  poimirlem3  37793  poimirlem4  37794  poimirlem16  37806  poimirlem19  37809  poimirlem20  37810  poimirlem23  37813  poimirlem31  37821  volsupnfl  37835  sdclem2  37912  fdc  37915  mettrifi  37927  iunincfi  45375  monoordxrv  45762  monoord2xrv  45764  fmul01lt1lem2  45868  limsupubuzlem  45993  dvnmul  46224  dvnprodlem3  46229  stoweidlem3  46284  stoweidlem11  46292  stoweidlem17  46298  stoweidlem34  46315  fourierdlem15  46403  fourierdlem25  46413  fourierdlem50  46437  fourierdlem52  46439  fourierdlem54  46441  fourierdlem65  46452  fourierdlem81  46468  fourierdlem92  46479  fourierdlem102  46489  fourierdlem111  46498  fourierdlem113  46500  fourierdlem114  46501  etransclem35  46550  sge0p1  46695  carageniuncllem1  46802  caratheodorylem1  46807  smfmullem4  47075  ssfz12  47597  elfzlble  47603  smonoord  47654  gpg3kgrtriexlem5  48370  gpg5grlim  48376  gpg5grlic  48377