Theorem fzss2 13701

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895  ‘cfv 6538  (class class class)co 7420  ℤ_≥cuz 12968  ...cfz 13642

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-pre-lttri 11277  ax-pre-lttrn 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-neg 11547  df-z 12697  df-uz 12969  df-fz 13643

This theorem is used by:  fzssp1  13704  elfz0add  13763  predfz  13790  fzoss2  13825  sermono  14180  seqsplit  14181  seqcaopr2  14184  seqf1olem2a  14186  seqf1olem2  14188  seqhomo  14195  seqz  14196  bcm1k  14462  seqcoll  14612  seqcoll2  14613  isercoll  15840  fsum0diaglem  15947  fsum0diag2  15954  cvgcmpce  15990  mertenslem1  16058  prodfn0  16068  prodfrec  16069  binomfallfaclem2  16211  bpoly4  16230  prmdvdsbc  16907  eulerthlem2  16964  pcfac  17082  vdwnnlem2  17179  strleun  17340  gsumzaddlem  20140  telgsumfzs  20208  freshmansdream  21885  imasdsf1olem  24697  plyaddlem1  26537  plymullem1  26538  coeeulem  26548  coeidlem  26561  coeid3  26564  coefv0  26572  coemulc  26579  vieta1lem2  26639  ppinprm  27484  chtnprm  27486  chpwordi  27489  chtublem  27543  bposlem1  27616  gausslemma2dlem2  27699  lgsquadlem3  27714  chebbnd1lem1  27801  vmadivsumb  27815  dchrvmasumiflem1  27833  mulog2sumlem2  27867  selbergb  27881  selberg2b  27884  chpdifbndlem1  27885  logdivbnd  27888  selberg3lem2  27890  pntrsumbnd  27898  pntlemq  27933  axlowdimlem16  29540  axlowdimlem17  29541  wlkres  30254  pfxwlk  30271  crctcshwlkn0lem2  30405  clwwlkvbij  30709  splfv3  33565  ballotlemimin  35184  ballotlemsdom  35190  ballotlemsel1i  35191  ballotlemsima  35194  ballotlemfrc  35205  ballotlemfrceq  35207  fzssfzo  35217  fsum2dsub  35282  erdszelem7  36048  erdszelem8  36049  elfzm12  36526  poimirlem1  38632  poimirlem2  38633  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem9  38640  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem22  38653  poimirlem23  38654  poimirlem24  38655  poimirlem26  38657  poimirlem27  38658  poimirlem28  38659  poimirlem31  38662  mettrifi  38784  eldiophb  43861  eldioph2lem2  43865  diophrex  43879  fmul01  46685  fmulcl  46686  dvnprodlem2  47050  stoweidlem11  47114  stoweidlem17  47120  stoweidlem26  47129  iccpartres  48593  iccpartipre  48596