Theorem fzss2 11618

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 11569	. . . . 5 |- ( k e. ( M ... K ) -> k e. ( ZZ>= ` M ) )
2	1	adantl 466	. . . 4 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> k e. ( ZZ>= ` M ) )
3		elfzuz3 11570	. . . . 5 |- ( k e. ( M ... K ) -> K e. ( ZZ>= ` k ) )
4		uztrn 10991	. . . . 5 |- ( ( N e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` k ) ) -> N e. ( ZZ>= ` k ) )
5	3, 4	sylan2 474	. . . 4 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> N e. ( ZZ>= ` k ) )
6		elfzuzb 11567	. . . 4 |- ( k e. ( M ... N ) <-> ( k e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` k ) ) )
7	2, 5, 6	sylanbrc 664	. . 3 |- ( ( N e. ( ZZ>= ` K ) /\ k e. ( M ... K ) ) -> k e. ( M ... N ) )
8	7	ex 434	. 2 |- ( N e. ( ZZ>= ` K ) -> ( k e. ( M ... K ) -> k e. ( M ... N ) ) )
9	8	ssrdv 3473	1 |- ( N e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... N ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1758   C_ wss 3439   ` cfv 5529  (class class class)co 6203   ZZ>=cuz 10975   ...cfz 11557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-cnex 9452  ax-resscn 9453  ax-pre-lttri 9470  ax-pre-lttrn 9471

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-1st 6690  df-2nd 6691  df-er 7214  df-en 7424  df-dom 7425  df-sdom 7426  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-neg 9712  df-z 10761  df-uz 10976  df-fz 11558

This theorem is referenced by:  fzssp1  11621  elfzelfzadd  11628  fzoss2  11697  sermono  11958  seqsplit  11959  seqcaopr2  11962  seqf1olem2a  11964  seqf1olem2  11966  seqhomo  11973  seqz  11974  bcm1k  12211  seqcoll  12337  seqcoll2  12338  isercoll  13266  fsum0diaglem  13364  fsum0diag2  13371  cvgcmpce  13402  mertenslem1  13465  eulerthlem2  13978  pcfac  14082  vdwnnlem2  14178  strlemor1  14387  strleun  14390  gsumzaddlem  16532  gsumzaddlemOLD  16534  imasdsf1olem  20083  plyaddlem1  21817  plymullem1  21818  coeeulem  21828  coeidlem  21841  coeid3  21844  coefv0  21851  coemulc  21858  vieta1lem2  21913  ppinprm  22626  chtnprm  22628  chpwordi  22631  chtublem  22686  bposlem1  22759  lgsquadlem3  22831  chebbnd1lem1  22854  vmadivsumb  22868  dchrvmasumiflem1  22886  mulog2sumlem2  22920  selbergb  22934  selberg2b  22937  chpdifbndlem1  22938  logdivbnd  22941  selberg3lem2  22943  pntrsumbnd  22951  pntlemq  22986  axlowdimlem16  23375  axlowdimlem17  23376  eupares  23768  eupath2lem3  23772  ballotlemimin  27052  ballotlemsdom  27058  ballotlemsel1i  27059  ballotlemsima  27062  ballotlemfrc  27073  ballotlemfrceq  27075  fzssfzo  27098  erdszelem7  27249  erdszelem8  27250  elfzm12  27484  prodfn0  27573  prodfrec  27574  binomfallfaclem2  27707  predfz  27828  bpoly4  28366  mettrifi  28821  eldiophb  29263  eldioph2lem2  29267  diophrex  29282  fmul01  29929  fmulcl  29930  stoweidlem11  29974  stoweidlem17  29980  stoweidlem26  29989  clwwlkvbij  30631  telescfzgsum  30982