Theorem fzss2 11048

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 11011	. . . . 5 |- ( k e. ( M ... K ) -> k e. ( ZZ>= ` M ) )
2	1	adantl 453	. . . 4 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> k e. ( ZZ>= ` M ) )
3		elfzuz3 11012	. . . . 5 |- ( k e. ( M ... K ) -> K e. ( ZZ>= ` k ) )
4		uztrn 10458	. . . . 5 |- ( ( N e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` k ) ) -> N e. ( ZZ>= ` k ) )
5	3, 4	sylan2 461	. . . 4 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> N e. ( ZZ>= ` k ) )
6		elfzuzb 11009	. . . 4 |- ( k e. ( M ... N ) <-> ( k e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` k ) ) )
7	2, 5, 6	sylanbrc 646	. . 3 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> k e. ( M ... N ) )
8	7	ex 424	. 2 |- ( N e. ( ZZ>= ` K ) -> ( k e. ( M ... K ) -> k e. ( M ... N ) ) )
9	8	ssrdv 3314	1 |- ( N e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... N ) )

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721   C_ wss 3280   ` cfv 5413  (class class class)co 6040   ZZ>=cuz 10444   ...cfz 10999

This theorem is referenced by:  fzssp1  11051  fzoss2  11118  sermono  11310  seqsplit  11311  seqcaopr2  11314  seqf1olem2a  11316  seqf1olem2  11318  seqhomo  11325  seqz  11326  bcm1k  11561  seqcoll  11667  seqcoll2  11668  isercoll  12416  fsum0diaglem  12515  fsum0diag2  12521  cvgcmpce  12552  mertenslem1  12616  eulerthlem2  13126  pcfac  13223  vdwnnlem2  13319  strlemor1  13511  strleun  13514  gsumzaddlem  15481  imasdsf1olem  18356  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeidlem  20109  coeid3  20112  coefv0  20119  coemulc  20126  vieta1lem2  20181  ppinprm  20888  chtnprm  20890  chpwordi  20893  chtublem  20948  bposlem1  21021  lgsquadlem3  21093  chebbnd1lem1  21116  vmadivsumb  21130  dchrvmasumiflem1  21148  mulog2sumlem2  21182  selbergb  21196  selberg2b  21199  chpdifbndlem1  21200  logdivbnd  21203  selberg3lem2  21205  pntrsumbnd  21213  pntlemq  21248  eupares  21650  eupath2lem3  21654  ballotlemimin  24716  ballotlemsdom  24722  ballotlemsel1i  24723  ballotlemsima  24726  ballotlemfrc  24737  ballotlemfrceq  24739  erdszelem7  24836  erdszelem8  24837  elfzm12  25065  prodfn0  25175  prodfrec  25176  binomfallfaclem2  25307  predfz  25417  axlowdimlem16  25800  axlowdimlem17  25801  bpoly4  26009  mettrifi  26353  eldiophb  26705  eldioph2lem2  26709  diophrex  26724  fmul01  27577  fmulcl  27578  stoweidlem11  27627  stoweidlem17  27633  stoweidlem26  27642  elfzelfzadd  27982  swrdccatin12lem3c  28023

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-pre-lttri 9020  ax-pre-lttrn 9021

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-neg 9250  df-z 10239  df-uz 10445  df-fz 11000