Theorem fzss2 12941

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 12898	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 484	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 12899	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12255	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 594	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 12896	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 585	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 415	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3972	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110   ⊆ wss 3935  ‘cfv 6349  (class class class)co 7150  ℤ_≥cuz 12237  ...cfz 12886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605  ax-pre-lttrn 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-neg 10867  df-z 11976  df-uz 12238  df-fz 12887

This theorem is referenced by:  fzssp1  12944  elfz0add  13000  predfz  13026  fzoss2  13059  sermono  13396  seqsplit  13397  seqcaopr2  13400  seqf1olem2a  13402  seqf1olem2  13404  seqhomo  13411  seqz  13412  bcm1k  13669  seqcoll  13816  seqcoll2  13817  isercoll  15018  fsum0diaglem  15125  fsum0diag2  15132  cvgcmpce  15167  mertenslem1  15234  prodfn0  15244  prodfrec  15245  binomfallfaclem2  15388  bpoly4  15407  eulerthlem2  16113  pcfac  16229  vdwnnlem2  16326  strleun  16585  gsumzaddlem  19035  telgsumfzs  19103  imasdsf1olem  22977  plyaddlem1  24797  plymullem1  24798  coeeulem  24808  coeidlem  24821  coeid3  24824  coefv0  24832  coemulc  24839  vieta1lem2  24894  ppinprm  25723  chtnprm  25725  chpwordi  25728  chtublem  25781  bposlem1  25854  gausslemma2dlem2  25937  lgsquadlem3  25952  chebbnd1lem1  26039  vmadivsumb  26053  dchrvmasumiflem1  26071  mulog2sumlem2  26105  selbergb  26119  selberg2b  26122  chpdifbndlem1  26123  logdivbnd  26126  selberg3lem2  26128  pntrsumbnd  26136  pntlemq  26171  axlowdimlem16  26737  axlowdimlem17  26738  wlkres  27446  crctcshwlkn0lem2  27583  clwwlkvbij  27886  prmdvdsbc  30526  splfv3  30627  freshmansdream  30854  ballotlemimin  31758  ballotlemsdom  31764  ballotlemsel1i  31765  ballotlemsima  31768  ballotlemfrc  31779  ballotlemfrceq  31781  fzssfzo  31804  fsum2dsub  31873  pfxwlk  32365  erdszelem7  32439  erdszelem8  32440  elfzm12  32913  poimirlem1  34887  poimirlem2  34888  poimirlem4  34890  poimirlem6  34892  poimirlem7  34893  poimirlem9  34895  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem22  34908  poimirlem23  34909  poimirlem24  34910  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  poimirlem31  34917  mettrifi  35026  eldiophb  39347  eldioph2lem2  39351  diophrex  39365  fmul01  41854  fmulcl  41855  dvnprodlem2  42225  stoweidlem11  42290  stoweidlem17  42296  stoweidlem26  42305  iccpartres  43572  iccpartipre  43575