Theorem fzss2 13595

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 13551	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 480	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13552	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12892	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 591	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13549	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 581	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 411	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3985	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099   ⊆ wss 3947  ‘cfv 6554  (class class class)co 7424  ℤ_≥cuz 12874  ...cfz 13538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-pre-lttri 11232  ax-pre-lttrn 11233

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8003  df-2nd 8004  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-neg 11497  df-z 12611  df-uz 12875  df-fz 13539

This theorem is referenced by:  fzssp1  13598  elfz0add  13654  predfz  13680  fzoss2  13714  sermono  14054  seqsplit  14055  seqcaopr2  14058  seqf1olem2a  14060  seqf1olem2  14062  seqhomo  14069  seqz  14070  bcm1k  14332  seqcoll  14483  seqcoll2  14484  isercoll  15672  fsum0diaglem  15780  fsum0diag2  15787  cvgcmpce  15822  mertenslem1  15888  prodfn0  15898  prodfrec  15899  binomfallfaclem2  16042  bpoly4  16061  prmdvdsbc  16728  eulerthlem2  16784  pcfac  16901  vdwnnlem2  16998  strleun  17159  gsumzaddlem  19919  telgsumfzs  19987  freshmansdream  21572  imasdsf1olem  24370  plyaddlem1  26240  plymullem1  26241  coeeulem  26251  coeidlem  26264  coeid3  26267  coefv0  26275  coemulc  26282  vieta1lem2  26339  ppinprm  27180  chtnprm  27182  chpwordi  27185  chtublem  27240  bposlem1  27313  gausslemma2dlem2  27396  lgsquadlem3  27411  chebbnd1lem1  27498  vmadivsumb  27512  dchrvmasumiflem1  27530  mulog2sumlem2  27564  selbergb  27578  selberg2b  27581  chpdifbndlem1  27582  logdivbnd  27585  selberg3lem2  27587  pntrsumbnd  27595  pntlemq  27630  axlowdimlem16  28891  axlowdimlem17  28892  wlkres  29607  crctcshwlkn0lem2  29745  clwwlkvbij  30046  splfv3  32822  ballotlemimin  34339  ballotlemsdom  34345  ballotlemsel1i  34346  ballotlemsima  34349  ballotlemfrc  34360  ballotlemfrceq  34362  fzssfzo  34385  fsum2dsub  34453  pfxwlk  34951  erdszelem7  35025  erdszelem8  35026  elfzm12  35503  poimirlem1  37322  poimirlem2  37323  poimirlem4  37325  poimirlem6  37327  poimirlem7  37328  poimirlem9  37330  poimirlem15  37336  poimirlem16  37337  poimirlem17  37338  poimirlem19  37340  poimirlem22  37343  poimirlem23  37344  poimirlem24  37345  poimirlem26  37347  poimirlem27  37348  poimirlem28  37349  poimirlem31  37352  mettrifi  37458  eldiophb  42414  eldioph2lem2  42418  diophrex  42432  fmul01  45201  fmulcl  45202  dvnprodlem2  45568  stoweidlem11  45632  stoweidlem17  45638  stoweidlem26  45647  iccpartres  46990  iccpartipre  46993