Theorem eluzfz2 13527

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 12848	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12853	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13514	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 686	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2099  ‘cfv 6542  (class class class)co 7414  ℤcz 12574  ℤ_≥cuz 12838  ...cfz 13502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-cnex 11180  ax-resscn 11181  ax-pre-lttri 11198

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7985  df-2nd 7986  df-er 8716  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-neg 11463  df-z 12575  df-uz 12839  df-fz 13503

This theorem is referenced by:  eluzfz2b  13528  elfzubelfz  13531  fzopth  13556  fzsuc  13566  fseq1p1m1  13593  fzm1  13599  fzneuz  13600  fzoend  13741  uzindi  13965  seqcl2  14003  seqfveq2  14007  seqshft2  14011  monoord  14015  monoord2  14016  seqsplit  14018  seqcaopr3  14020  seqf1olem2a  14023  seqf1olem1  14024  seqf1olem2  14025  seqid2  14031  seqhomo  14032  seqcoll  14443  seqcoll2  14444  wrdeqs1cat  14688  pfxccatin12lem2  14699  pfxccatin12lem3  14700  splid  14721  spllen  14722  splval2  14725  summolem2a  15679  fsumm1  15715  telfsumo  15766  telfsumo2  15767  fsumparts  15770  prodfn0  15858  prodfrec  15859  prodmolem2a  15896  fprodm1  15929  sadadd  16427  sadass  16431  smuval2  16442  vdwlem6  16940  efgredleme  19682  efgredlemc  19684  efgcpbllemb  19694  frgpuplem  19711  telgsumfzslem  19927  telgsumfzs  19928  pmatcollpw3fi1lem1  22662  chfacfisf  22730  chfacfisfcpmat  22731  iscmet3lem1  25193  iscmet3lem2  25194  voliunlem1  25453  volsup  25459  mbfi1fseqlem3  25621  wilthlem2  26975  wilthlem3  26976  chtub  27119  dchrisum0flb  27417  pntpbnd1  27493  pntlemf  27512  spthonepeq  29540  wwlksnext  29678  2clwwlk2clwwlklem  30130  clwwlknonclwlknonf1o  30146  wrdsplex  32630  cycpmco2f1  32810  submatres  33330  madjusmdetlem1  33351  madjusmdetlem2  33352  madjusmdetlem3  33353  madjusmdetlem4  33354  ballotlemfc0  34035  ballotlemfcc  34036  ballotlemfrci  34070  gsumnunsn  34096  swrdrevpfx  34649  cvmliftlem10  34827  supfz  35246  fwddifnp1  35684  poimirlem3  37018  poimirlem4  37019  poimirlem16  37031  poimirlem19  37034  poimirlem20  37035  poimirlem23  37038  poimirlem31  37046  volsupnfl  37060  sdclem2  37137  fdc  37140  mettrifi  37152  iunincfi  44373  monoordxrv  44777  monoord2xrv  44779  fmul01lt1lem2  44886  limsupubuzlem  45013  dvnmul  45244  dvnprodlem3  45249  stoweidlem3  45304  stoweidlem11  45312  stoweidlem17  45318  stoweidlem34  45335  fourierdlem15  45423  fourierdlem25  45433  fourierdlem50  45457  fourierdlem52  45459  fourierdlem54  45461  fourierdlem65  45472  fourierdlem81  45488  fourierdlem92  45499  fourierdlem102  45509  fourierdlem111  45518  fourierdlem113  45520  fourierdlem114  45521  etransclem35  45570  sge0p1  45715  carageniuncllem1  45822  caratheodorylem1  45827  smfmullem4  46095  ssfz12  46607  elfzlble  46613  smonoord  46624