Theorem fzss2 13698

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 13652	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 487	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13653	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12983	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 605	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13650	. . . 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 12965  ...cfz 13639

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 11256  ax-resscn 11257  ax-pre-lttri 11274  ax-pre-lttrn 11275

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 4584  df-pr 4586  df-op 4590  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 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-neg 11544  df-z 12694  df-uz 12966  df-fz 13640

This theorem is used by:  fzssp1  13701  elfz0add  13760  predfz  13787  fzoss2  13822  sermono  14177  seqsplit  14178  seqcaopr2  14181  seqf1olem2a  14183  seqf1olem2  14185  seqhomo  14192  seqz  14193  bcm1k  14459  seqcoll  14609  seqcoll2  14610  isercoll  15835  fsum0diaglem  15942  fsum0diag2  15949  cvgcmpce  15985  mertenslem1  16053  prodfn0  16063  prodfrec  16064  binomfallfaclem2  16206  bpoly4  16225  prmdvdsbc  16902  eulerthlem2  16959  pcfac  17077  vdwnnlem2  17174  strleun  17335  gsumzaddlem  20135  telgsumfzs  20203  freshmansdream  21880  imasdsf1olem  24692  plyaddlem1  26532  plymullem1  26533  coeeulem  26543  coeidlem  26556  coeid3  26559  coefv0  26567  coemulc  26574  vieta1lem2  26634  ppinprm  27479  chtnprm  27481  chpwordi  27484  chtublem  27538  bposlem1  27611  gausslemma2dlem2  27694  lgsquadlem3  27709  chebbnd1lem1  27796  vmadivsumb  27810  dchrvmasumiflem1  27828  mulog2sumlem2  27862  selbergb  27876  selberg2b  27879  chpdifbndlem1  27880  logdivbnd  27883  selberg3lem2  27885  pntrsumbnd  27893  pntlemq  27928  axlowdimlem16  29535  axlowdimlem17  29536  wlkres  30249  pfxwlk  30266  crctcshwlkn0lem2  30400  clwwlkvbij  30704  splfv3  33519  ballotlemimin  35138  ballotlemsdom  35144  ballotlemsel1i  35145  ballotlemsima  35148  ballotlemfrc  35159  ballotlemfrceq  35161  fzssfzo  35171  fsum2dsub  35236  erdszelem7  35962  erdszelem8  35963  elfzm12  36440  poimirlem1  38540  poimirlem2  38541  poimirlem4  38543  poimirlem6  38545  poimirlem7  38546  poimirlem9  38548  poimirlem15  38554  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  poimirlem31  38570  mettrifi  38692  eldiophb  43768  eldioph2lem2  43772  diophrex  43786  fmul01  46592  fmulcl  46593  dvnprodlem2  46957  stoweidlem11  47021  stoweidlem17  47027  stoweidlem26  47036  iccpartres  48500  iccpartipre  48503