Theorem fzss2 12786

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 12743	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 482	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 12744	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12099	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 592	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 12741	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 583	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 413	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3890	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2079   ⊆ wss 3854  ‘cfv 6217  (class class class)co 7007  ℤ_≥cuz 12082  ...cfz 12731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-resscn 10429  ax-pre-lttri 10446  ax-pre-lttrn 10447

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-ov 7010  df-oprab 7011  df-mpo 7012  df-1st 7536  df-2nd 7537  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516  df-neg 10709  df-z 11819  df-uz 12083  df-fz 12732

This theorem is referenced by:  fzssp1  12789  elfz0add  12845  predfz  12871  fzoss2  12903  sermono  13240  seqsplit  13241  seqcaopr2  13244  seqf1olem2a  13246  seqf1olem2  13248  seqhomo  13255  seqz  13256  bcm1k  13513  seqcoll  13658  seqcoll2  13659  isercoll  14846  fsum0diaglem  14952  fsum0diag2  14959  cvgcmpce  14994  mertenslem1  15061  prodfn0  15071  prodfrec  15072  binomfallfaclem2  15215  bpoly4  15234  eulerthlem2  15936  pcfac  16052  vdwnnlem2  16149  strleun  16408  gsumzaddlem  18749  telgsumfzs  18814  imasdsf1olem  22654  plyaddlem1  24474  plymullem1  24475  coeeulem  24485  coeidlem  24498  coeid3  24501  coefv0  24509  coemulc  24516  vieta1lem2  24571  ppinprm  25399  chtnprm  25401  chpwordi  25404  chtublem  25457  bposlem1  25530  gausslemma2dlem2  25613  lgsquadlem3  25628  chebbnd1lem1  25715  vmadivsumb  25729  dchrvmasumiflem1  25747  mulog2sumlem2  25781  selbergb  25795  selberg2b  25798  chpdifbndlem1  25799  logdivbnd  25802  selberg3lem2  25804  pntrsumbnd  25812  pntlemq  25847  axlowdimlem16  26414  axlowdimlem17  26415  wlkres  27123  wlkresOLD  27125  crctcshwlkn0lem2  27264  clwwlkvbij  27567  prmdvdsbc  30187  freshmansdream  30468  ballotlemimin  31336  ballotlemsdom  31342  ballotlemsel1i  31343  ballotlemsima  31346  ballotlemfrc  31357  ballotlemfrceq  31359  fzssfzo  31382  fsum2dsub  31451  erdszelem7  32008  erdszelem8  32009  elfzm12  32471  poimirlem1  34370  poimirlem2  34371  poimirlem4  34373  poimirlem6  34375  poimirlem7  34376  poimirlem9  34378  poimirlem15  34384  poimirlem16  34385  poimirlem17  34386  poimirlem19  34388  poimirlem22  34391  poimirlem23  34392  poimirlem24  34393  poimirlem26  34395  poimirlem27  34396  poimirlem28  34397  poimirlem31  34400  mettrifi  34510  eldiophb  38789  eldioph2lem2  38793  diophrex  38808  fmul01  41357  fmulcl  41358  dvnprodlem2  41727  stoweidlem11  41792  stoweidlem17  41798  stoweidlem26  41807  iccpartres  43014  iccpartipre  43017