Theorem fzss2 11867

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.)

Assertion

Ref	Expression
fzss2	|- ( N e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... N ) )

Proof of Theorem fzss2

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzuz 11825	. . . . 5 |- ( k e. ( M ... K ) -> k e. ( ZZ>= ` M ) )
2	1	adantl 472	. . . 4 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> k e. ( ZZ>= ` M ) )
3		elfzuz3 11826	. . . . 5 |- ( k e. ( M ... K ) -> K e. ( ZZ>= ` k ) )
4		uztrn 11204	. . . . 5 |- ( ( N e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` k ) ) -> N e. ( ZZ>= ` k ) )
5	3, 4	sylan2 481	. . . 4 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> N e. ( ZZ>= ` k ) )
6		elfzuzb 11823	. . . 4 |- ( k e. ( M ... N ) <-> ( k e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` k ) ) )
7	2, 5, 6	sylanbrc 675	. . 3 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> k e. ( M ... N ) )
8	7	ex 440	. 2 |- ( N e. ( ZZ>= ` K ) -> ( k e. ( M ... K ) -> k e. ( M ... N ) ) )
9	8	ssrdv 3450	1 |- ( N e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... N ) )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898   C_ wss 3416   ` cfv 5601  (class class class)co 6315   ZZ>=cuz 11188   ...cfz 11813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-pre-lttri 9639  ax-pre-lttrn 9640

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-1st 6820  df-2nd 6821  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-neg 9889  df-z 10967  df-uz 11189  df-fz 11814

This theorem is referenced by:  fzssp1  11870  elfz0add  11920  elfz0addOLD  11921  predfz  11945  fzoss2  11977  sermono  12277  seqsplit  12278  seqcaopr2  12281  seqf1olem2a  12283  seqf1olem2  12285  seqhomo  12292  seqz  12293  bcm1k  12532  seqcoll  12660  seqcoll2  12661  isercoll  13780  fsum0diaglem  13886  fsum0diag2  13893  cvgcmpce  13927  mertenslem1  13989  prodfn0  13999  prodfrec  14000  binomfallfaclem2  14142  bpoly4  14161  eulerthlem2  14779  pcfac  14893  vdwnnlem2  14995  strlemor1  15266  strleun  15269  gsumzaddlem  17603  telgsumfzs  17668  imasdsf1olem  21437  plyaddlem1  23216  plymullem1  23217  coeeulem  23227  coeidlem  23240  coeid3  23243  coefv0  23251  coemulc  23258  vieta1lem2  23313  ppinprm  24128  chtnprm  24130  chpwordi  24133  chtublem  24188  bposlem1  24261  lgsquadlem3  24333  chebbnd1lem1  24356  vmadivsumb  24370  dchrvmasumiflem1  24388  mulog2sumlem2  24422  selbergb  24436  selberg2b  24439  chpdifbndlem1  24440  logdivbnd  24443  selberg3lem2  24445  pntrsumbnd  24453  pntlemq  24488  axlowdimlem16  25036  axlowdimlem17  25037  clwwlkvbij  25578  eupares  25752  eupath2lem3  25756  ballotlemimin  29387  ballotlemsdom  29393  ballotlemsel1i  29394  ballotlemsima  29397  ballotlemfrc  29408  ballotlemfrceq  29410  ballotlemiminOLD  29425  ballotlemsdomOLD  29431  ballotlemsel1iOLD  29432  ballotlemsimaOLD  29435  ballotlemfrcOLD  29446  ballotlemfrceqOLD  29448  fzssfzo  29471  erdszelem7  29969  erdszelem8  29970  elfzm12  30368  poimirlem1  31986  poimirlem2  31987  poimirlem4  31989  poimirlem6  31991  poimirlem7  31992  poimirlem9  31994  poimirlem15  32000  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem22  32007  poimirlem23  32008  poimirlem24  32009  poimirlem26  32011  poimirlem27  32012  poimirlem28  32013  poimirlem31  32016  mettrifi  32131  eldiophb  35644  eldioph2lem2  35648  diophrex  35663  fmul01  37696  fmulcl  37697  dvnprodlem2  37860  stoweidlem11  37909  stoweidlem17  37915  stoweidlem26  37924  iccpartres  38770  iccpartipre  38773