Theorem fzss2 13509

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	⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Proof of Theorem fzss2

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzuz 13465	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 481	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13466	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12797	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 594	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13463	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 584	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 412	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3928	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6492  (class class class)co 7360  ℤ_≥cuz 12779  ...cfz 13452

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 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-neg 11371  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  fzssp1  13512  elfz0add  13571  predfz  13598  fzoss2  13633  sermono  13987  seqsplit  13988  seqcaopr2  13991  seqf1olem2a  13993  seqf1olem2  13995  seqhomo  14002  seqz  14003  bcm1k  14268  seqcoll  14417  seqcoll2  14418  isercoll  15621  fsum0diaglem  15729  fsum0diag2  15736  cvgcmpce  15772  mertenslem1  15840  prodfn0  15850  prodfrec  15851  binomfallfaclem2  15996  bpoly4  16015  prmdvdsbc  16687  eulerthlem2  16743  pcfac  16861  vdwnnlem2  16958  strleun  17118  gsumzaddlem  19887  telgsumfzs  19955  freshmansdream  21564  imasdsf1olem  24348  plyaddlem1  26188  plymullem1  26189  coeeulem  26199  coeidlem  26212  coeid3  26215  coefv0  26223  coemulc  26230  vieta1lem2  26288  ppinprm  27129  chtnprm  27131  chpwordi  27134  chtublem  27188  bposlem1  27261  gausslemma2dlem2  27344  lgsquadlem3  27359  chebbnd1lem1  27446  vmadivsumb  27460  dchrvmasumiflem1  27478  mulog2sumlem2  27512  selbergb  27526  selberg2b  27529  chpdifbndlem1  27530  logdivbnd  27533  selberg3lem2  27535  pntrsumbnd  27543  pntlemq  27578  axlowdimlem16  29040  axlowdimlem17  29041  wlkres  29752  crctcshwlkn0lem2  29894  clwwlkvbij  30198  splfv3  33033  ballotlemimin  34666  ballotlemsdom  34672  ballotlemsel1i  34673  ballotlemsima  34676  ballotlemfrc  34687  ballotlemfrceq  34689  fzssfzo  34699  fsum2dsub  34767  pfxwlk  35322  erdszelem7  35395  erdszelem8  35396  elfzm12  35873  poimirlem1  37956  poimirlem2  37957  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem31  37986  mettrifi  38092  eldiophb  43203  eldioph2lem2  43207  diophrex  43221  fmul01  46028  fmulcl  46029  dvnprodlem2  46393  stoweidlem11  46457  stoweidlem17  46463  stoweidlem26  46472  iccpartres  47890  iccpartipre  47893