Theorem fzss2 13537

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 13493	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 482	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13494	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12836	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 593	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13491	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 583	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 413	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3987	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3947  ‘cfv 6540  (class class class)co 7405  ℤ_≥cuz 12818  ...cfz 13480

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-neg 11443  df-z 12555  df-uz 12819  df-fz 13481

This theorem is referenced by:  fzssp1  13540  elfz0add  13596  predfz  13622  fzoss2  13656  sermono  13996  seqsplit  13997  seqcaopr2  14000  seqf1olem2a  14002  seqf1olem2  14004  seqhomo  14011  seqz  14012  bcm1k  14271  seqcoll  14421  seqcoll2  14422  isercoll  15610  fsum0diaglem  15718  fsum0diag2  15725  cvgcmpce  15760  mertenslem1  15826  prodfn0  15836  prodfrec  15837  binomfallfaclem2  15980  bpoly4  15999  eulerthlem2  16711  pcfac  16828  vdwnnlem2  16925  strleun  17086  gsumzaddlem  19783  telgsumfzs  19851  imasdsf1olem  23870  plyaddlem1  25718  plymullem1  25719  coeeulem  25729  coeidlem  25742  coeid3  25745  coefv0  25753  coemulc  25760  vieta1lem2  25815  ppinprm  26645  chtnprm  26647  chpwordi  26650  chtublem  26703  bposlem1  26776  gausslemma2dlem2  26859  lgsquadlem3  26874  chebbnd1lem1  26961  vmadivsumb  26975  dchrvmasumiflem1  26993  mulog2sumlem2  27027  selbergb  27041  selberg2b  27044  chpdifbndlem1  27045  logdivbnd  27048  selberg3lem2  27050  pntrsumbnd  27058  pntlemq  27093  axlowdimlem16  28204  axlowdimlem17  28205  wlkres  28916  crctcshwlkn0lem2  29054  clwwlkvbij  29355  prmdvdsbc  32009  splfv3  32109  freshmansdream  32369  ballotlemimin  33492  ballotlemsdom  33498  ballotlemsel1i  33499  ballotlemsima  33502  ballotlemfrc  33513  ballotlemfrceq  33515  fzssfzo  33538  fsum2dsub  33607  pfxwlk  34102  erdszelem7  34176  erdszelem8  34177  elfzm12  34648  poimirlem1  36477  poimirlem2  36478  poimirlem4  36480  poimirlem6  36482  poimirlem7  36483  poimirlem9  36485  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem19  36495  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  poimirlem31  36507  mettrifi  36613  eldiophb  41480  eldioph2lem2  41484  diophrex  41498  fmul01  44282  fmulcl  44283  dvnprodlem2  44649  stoweidlem11  44713  stoweidlem17  44719  stoweidlem26  44728  iccpartres  46072  iccpartipre  46075