Theorem fzss2 13611

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 13566	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 487	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13567	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12898	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 605	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13564	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 595	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 418	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3946	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3908  ‘cfv 6543  (class class class)co 7423  ℤ_≥cuz 12880  ...cfz 13553

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-pre-lttri 11192  ax-pre-lttrn 11193

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-neg 11462  df-z 12610  df-uz 12881  df-fz 13554

This theorem is used by:  fzssp1  13614  elfz0add  13673  predfz  13700  fzoss2  13735  sermono  14090  seqsplit  14091  seqcaopr2  14094  seqf1olem2a  14096  seqf1olem2  14098  seqhomo  14105  seqz  14106  bcm1k  14371  seqcoll  14521  seqcoll2  14522  isercoll  15745  fsum0diaglem  15853  fsum0diag2  15860  cvgcmpce  15896  mertenslem1  15964  prodfn0  15974  prodfrec  15975  binomfallfaclem2  16119  bpoly4  16138  prmdvdsbc  16810  eulerthlem2  16866  pcfac  16984  vdwnnlem2  17081  strleun  17242  gsumzaddlem  20022  telgsumfzs  20090  freshmansdream  21761  imasdsf1olem  24567  plyaddlem1  26407  plymullem1  26408  coeeulem  26418  coeidlem  26431  coeid3  26434  coefv0  26442  coemulc  26449  vieta1lem2  26509  ppinprm  27353  chtnprm  27355  chpwordi  27358  chtublem  27412  bposlem1  27485  gausslemma2dlem2  27568  lgsquadlem3  27583  chebbnd1lem1  27670  vmadivsumb  27684  dchrvmasumiflem1  27702  mulog2sumlem2  27736  selbergb  27750  selberg2b  27753  chpdifbndlem1  27754  logdivbnd  27757  selberg3lem2  27759  pntrsumbnd  27767  pntlemq  27802  axlowdimlem16  29344  axlowdimlem17  29345  wlkres  30055  crctcshwlkn0lem2  30197  clwwlkvbij  30501  splfv3  33309  ballotlemimin  34928  ballotlemsdom  34934  ballotlemsel1i  34935  ballotlemsima  34938  ballotlemfrc  34949  ballotlemfrceq  34951  fzssfzo  34961  fsum2dsub  35026  pfxwlk  35637  erdszelem7  35710  erdszelem8  35711  elfzm12  36188  poimirlem1  38313  poimirlem2  38314  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem9  38321  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  poimirlem31  38343  mettrifi  38449  eldiophb  43529  eldioph2lem2  43533  diophrex  43547  fmul01  46337  fmulcl  46338  dvnprodlem2  46702  stoweidlem11  46766  stoweidlem17  46772  stoweidlem26  46781  iccpartres  48208  iccpartipre  48211