Theorem eluzfz2 13462

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6502  (class class class)co 7370  ℤcz 12502  ℤ_≥cuz 12765  ...cfz 13437

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 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-pre-lttri 11114

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-1st 7945  df-2nd 7946  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-neg 11381  df-z 12503  df-uz 12766  df-fz 13438

This theorem is referenced by:  eluzfz2b  13463  elfzubelfz  13466  fzopth  13491  fzsuc  13501  fseq1p1m1  13528  fzm1  13537  fzneuz  13538  fzoend  13687  uzindi  13919  seqcl2  13957  seqfveq2  13961  seqshft2  13965  monoord  13969  monoord2  13970  seqsplit  13972  seqcaopr3  13974  seqf1olem2a  13977  seqf1olem1  13978  seqf1olem2  13979  seqid2  13985  seqhomo  13986  seqcoll  14401  seqcoll2  14402  wrdeqs1cat  14657  pfxccatin12lem2  14668  pfxccatin12lem3  14669  splid  14690  spllen  14691  splval2  14694  summolem2a  15652  fsumm1  15688  telfsumo  15739  telfsumo2  15740  fsumparts  15743  prodfn0  15831  prodfrec  15832  prodmolem2a  15871  fprodm1  15904  sadadd  16408  sadass  16412  smuval2  16423  vdwlem6  16928  efgredleme  19689  efgredlemc  19691  efgcpbllemb  19701  frgpuplem  19718  telgsumfzslem  19934  telgsumfzs  19935  pmatcollpw3fi1lem1  22747  chfacfisf  22815  chfacfisfcpmat  22816  iscmet3lem1  25264  iscmet3lem2  25265  voliunlem1  25524  volsup  25530  mbfi1fseqlem3  25691  wilthlem2  27052  wilthlem3  27053  chtub  27196  dchrisum0flb  27494  pntpbnd1  27570  pntlemf  27589  spthonepeq  29843  wwlksnext  29984  2clwwlk2clwwlklem  30439  clwwlknonclwlknonf1o  30455  wrdsplex  33035  gsummptfzsplitra  33158  cycpmco2f1  33224  submatres  33990  madjusmdetlem1  34011  madjusmdetlem2  34012  madjusmdetlem3  34013  madjusmdetlem4  34014  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemfrci  34712  gsumnunsn  34725  swrdrevpfx  35339  cvmliftlem10  35516  supfz  35951  fwddifnp1  36387  poimirlem3  37903  poimirlem4  37904  poimirlem16  37916  poimirlem19  37919  poimirlem20  37920  poimirlem23  37923  poimirlem31  37931  volsupnfl  37945  sdclem2  38022  fdc  38025  mettrifi  38037  iunincfi  45482  monoordxrv  45868  monoord2xrv  45870  fmul01lt1lem2  45974  limsupubuzlem  46099  dvnmul  46330  dvnprodlem3  46335  stoweidlem3  46390  stoweidlem11  46398  stoweidlem17  46404  stoweidlem34  46421  fourierdlem15  46509  fourierdlem25  46519  fourierdlem50  46543  fourierdlem52  46545  fourierdlem54  46547  fourierdlem65  46558  fourierdlem81  46574  fourierdlem92  46585  fourierdlem102  46595  fourierdlem111  46604  fourierdlem113  46606  fourierdlem114  46607  etransclem35  46656  sge0p1  46801  carageniuncllem1  46908  caratheodorylem1  46913  smfmullem4  47181  ssfz12  47703  elfzlble  47709  smonoord  47760  gpg3kgrtriexlem5  48476  gpg5grlim  48482  gpg5grlic  48483