Theorem eluzfz2 13481

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 12793	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12798	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13468	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 694	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2121  ‘cfv 6489  (class class class)co 7360  ℤcz 12519  ℤ_≥cuz 12783  ...cfz 13456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-neg 11375  df-z 12520  df-uz 12784  df-fz 13457

This theorem is referenced by:  eluzfz2b  13482  elfzubelfz  13485  fzopth  13510  fzsuc  13520  fseq1p1m1  13547  fzm1  13556  fzneuz  13557  fzoend  13707  uzindi  13939  seqcl2  13977  seqfveq2  13981  seqshft2  13985  monoord  13989  monoord2  13990  seqsplit  13992  seqcaopr3  13994  seqf1olem2a  13997  seqf1olem1  13998  seqf1olem2  13999  seqid2  14005  seqhomo  14006  seqcoll  14421  seqcoll2  14422  wrdeqs1cat  14677  pfxccatin12lem2  14688  pfxccatin12lem3  14689  splid  14710  spllen  14711  splval2  14714  summolem2a  15672  fsumm1  15708  telfsumo  15760  telfsumo2  15761  fsumparts  15764  prodfn0  15854  prodfrec  15855  prodmolem2a  15894  fprodm1  15927  sadadd  16431  sadass  16435  smuval2  16446  vdwlem6  16952  efgredleme  19713  efgredlemc  19715  efgcpbllemb  19725  frgpuplem  19742  telgsumfzslem  19958  telgsumfzs  19959  pmatcollpw3fi1lem1  22773  chfacfisf  22841  chfacfisfcpmat  22842  iscmet3lem1  25280  iscmet3lem2  25281  voliunlem1  25539  volsup  25545  mbfi1fseqlem3  25706  wilthlem2  27054  wilthlem3  27055  chtub  27197  dchrisum0flb  27495  pntpbnd1  27571  pntlemf  27590  spthonepeq  29842  wwlksnext  29983  2clwwlk2clwwlklem  30438  clwwlknonclwlknonf1o  30454  wrdsplex  33019  gsummptfzsplitra  33143  cycpmco2f1  33209  submatres  34002  madjusmdetlem1  34023  madjusmdetlem2  34024  madjusmdetlem3  34025  madjusmdetlem4  34026  ballotlemfc0  34689  ballotlemfcc  34690  ballotlemfrci  34724  gsumnunsn  34737  swrdrevpfx  35360  cvmliftlem10  35537  supfz  35972  fwddifnp1  36408  poimirlem3  38005  poimirlem4  38006  poimirlem16  38018  poimirlem19  38021  poimirlem20  38022  poimirlem23  38025  poimirlem31  38033  volsupnfl  38047  sdclem2  38124  fdc  38127  mettrifi  38139  iunincfi  45555  monoordxrv  45938  monoord2xrv  45940  fmul01lt1lem2  46044  limsupubuzlem  46169  dvnmul  46400  dvnprodlem3  46405  stoweidlem3  46460  stoweidlem11  46468  stoweidlem17  46474  stoweidlem34  46491  fourierdlem15  46579  fourierdlem25  46589  fourierdlem50  46613  fourierdlem52  46615  fourierdlem54  46617  fourierdlem65  46628  fourierdlem81  46644  fourierdlem92  46655  fourierdlem102  46665  fourierdlem111  46674  fourierdlem113  46676  fourierdlem114  46677  etransclem35  46726  sge0p1  46871  carageniuncllem1  46978  caratheodorylem1  46983  smfmullem4  47251  ssfz12  47791  elfzlble  47797  smonoord  47854  gpg3kgrtriexlem5  48592  gpg5grlim  48598  gpg5grlic  48599