Theorem fzss2 13594

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 13549	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 486	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13550	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12881	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 604	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13547	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 594	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 417	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3944	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3906  ‘cfv 6538  (class class class)co 7412  ℤ_≥cuz 12863  ...cfz 13536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-pre-lttri 11175  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7987  df-2nd 7988  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-neg 11445  df-z 12593  df-uz 12864  df-fz 13537

This theorem is referenced by:  fzssp1  13597  elfz0add  13656  predfz  13683  fzoss2  13718  sermono  14072  seqsplit  14073  seqcaopr2  14076  seqf1olem2a  14078  seqf1olem2  14080  seqhomo  14087  seqz  14088  bcm1k  14353  seqcoll  14503  seqcoll2  14504  isercoll  15721  fsum0diaglem  15829  fsum0diag2  15836  cvgcmpce  15872  mertenslem1  15940  prodfn0  15950  prodfrec  15951  binomfallfaclem2  16095  bpoly4  16114  prmdvdsbc  16786  eulerthlem2  16842  pcfac  16960  vdwnnlem2  17057  strleun  17218  gsumzaddlem  19992  telgsumfzs  20060  freshmansdream  21705  imasdsf1olem  24511  plyaddlem1  26351  plymullem1  26352  coeeulem  26362  coeidlem  26375  coeid3  26378  coefv0  26386  coemulc  26393  vieta1lem2  26453  ppinprm  27297  chtnprm  27299  chpwordi  27302  chtublem  27356  bposlem1  27429  gausslemma2dlem2  27512  lgsquadlem3  27527  chebbnd1lem1  27614  vmadivsumb  27628  dchrvmasumiflem1  27646  mulog2sumlem2  27680  selbergb  27694  selberg2b  27697  chpdifbndlem1  27698  logdivbnd  27701  selberg3lem2  27703  pntrsumbnd  27711  pntlemq  27746  axlowdimlem16  29288  axlowdimlem17  29289  wlkres  29999  crctcshwlkn0lem2  30141  clwwlkvbij  30445  splfv3  33259  ballotlemimin  34877  ballotlemsdom  34883  ballotlemsel1i  34884  ballotlemsima  34887  ballotlemfrc  34898  ballotlemfrceq  34900  fzssfzo  34910  fsum2dsub  34975  pfxwlk  35597  erdszelem7  35670  erdszelem8  35671  elfzm12  36148  poimirlem1  38253  poimirlem2  38254  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem9  38261  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  poimirlem31  38283  mettrifi  38389  eldiophb  43471  eldioph2lem2  43475  diophrex  43489  fmul01  46279  fmulcl  46280  dvnprodlem2  46644  stoweidlem11  46708  stoweidlem17  46714  stoweidlem26  46723  iccpartres  48150  iccpartipre  48153