Theorem eluzfz2 13273

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 12601	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12606	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13260	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 684	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  ℤcz 12328  ℤ_≥cuz 12591  ...cfz 13248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-pre-lttri 10954

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-neg 11217  df-z 12329  df-uz 12592  df-fz 13249

This theorem is referenced by:  eluzfz2b  13274  elfzubelfz  13277  fzopth  13302  fzsuc  13312  fseq1p1m1  13339  fzm1  13345  fzneuz  13346  fzoend  13487  uzindi  13711  seqcl2  13750  seqfveq2  13754  seqshft2  13758  monoord  13762  monoord2  13763  seqsplit  13765  seqcaopr3  13767  seqf1olem2a  13770  seqf1olem1  13771  seqf1olem2  13772  seqid2  13778  seqhomo  13779  seqcoll  14187  seqcoll2  14188  wrdeqs1cat  14442  pfxccatin12lem2  14453  pfxccatin12lem3  14454  splid  14475  spllen  14476  splval2  14479  summolem2a  15436  fsumm1  15472  telfsumo  15523  telfsumo2  15524  fsumparts  15527  prodfn0  15615  prodfrec  15616  prodmolem2a  15653  fprodm1  15686  sadadd  16183  sadass  16187  smuval2  16198  vdwlem6  16696  efgredleme  19358  efgredlemc  19360  efgcpbllemb  19370  frgpuplem  19387  telgsumfzslem  19598  telgsumfzs  19599  pmatcollpw3fi1lem1  21944  chfacfisf  22012  chfacfisfcpmat  22013  iscmet3lem1  24464  iscmet3lem2  24465  voliunlem1  24723  volsup  24729  mbfi1fseqlem3  24891  wilthlem2  26227  wilthlem3  26228  chtub  26369  dchrisum0flb  26667  pntpbnd1  26743  pntlemf  26762  spthonepeq  28129  wwlksnext  28267  2clwwlk2clwwlklem  28719  clwwlknonclwlknonf1o  28735  wrdsplex  31221  cycpmco2f1  31400  submatres  31765  madjusmdetlem1  31786  madjusmdetlem2  31787  madjusmdetlem3  31788  madjusmdetlem4  31789  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemfrci  32503  gsumnunsn  32529  swrdrevpfx  33087  cvmliftlem10  33265  supfz  33703  fwddifnp1  34476  poimirlem3  35789  poimirlem4  35790  poimirlem16  35802  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem31  35817  volsupnfl  35831  sdclem2  35909  fdc  35912  mettrifi  35924  iunincfi  42651  monoordxrv  43029  monoord2xrv  43031  fmul01lt1lem2  43133  limsupubuzlem  43260  dvnmul  43491  dvnprodlem3  43496  stoweidlem3  43551  stoweidlem11  43559  stoweidlem17  43565  stoweidlem34  43582  fourierdlem15  43670  fourierdlem25  43680  fourierdlem50  43704  fourierdlem52  43706  fourierdlem54  43708  fourierdlem65  43719  fourierdlem81  43735  fourierdlem92  43746  fourierdlem102  43756  fourierdlem111  43765  fourierdlem113  43767  fourierdlem114  43768  etransclem35  43817  sge0p1  43959  carageniuncllem1  44066  caratheodorylem1  44071  smfmullem4  44339  ssfz12  44817  elfzlble  44823  smonoord  44834