Theorem fzss2 13467

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 13423	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 481	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13424	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12753	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 593	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13421	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 583	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 412	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3941	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3903  ‘cfv 6482  (class class class)co 7349  ℤ_≥cuz 12735  ...cfz 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1st 7924  df-2nd 7925  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-neg 11350  df-z 12472  df-uz 12736  df-fz 13411

This theorem is referenced by:  fzssp1  13470  elfz0add  13529  predfz  13556  fzoss2  13590  sermono  13941  seqsplit  13942  seqcaopr2  13945  seqf1olem2a  13947  seqf1olem2  13949  seqhomo  13956  seqz  13957  bcm1k  14222  seqcoll  14371  seqcoll2  14372  isercoll  15575  fsum0diaglem  15683  fsum0diag2  15690  cvgcmpce  15725  mertenslem1  15791  prodfn0  15801  prodfrec  15802  binomfallfaclem2  15947  bpoly4  15966  prmdvdsbc  16637  eulerthlem2  16693  pcfac  16811  vdwnnlem2  16908  strleun  17068  gsumzaddlem  19800  telgsumfzs  19868  freshmansdream  21481  imasdsf1olem  24259  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coeidlem  26140  coeid3  26143  coefv0  26151  coemulc  26158  vieta1lem2  26217  ppinprm  27060  chtnprm  27062  chpwordi  27065  chtublem  27120  bposlem1  27193  gausslemma2dlem2  27276  lgsquadlem3  27291  chebbnd1lem1  27378  vmadivsumb  27392  dchrvmasumiflem1  27410  mulog2sumlem2  27444  selbergb  27458  selberg2b  27461  chpdifbndlem1  27462  logdivbnd  27465  selberg3lem2  27467  pntrsumbnd  27475  pntlemq  27510  axlowdimlem16  28906  axlowdimlem17  28907  wlkres  29618  crctcshwlkn0lem2  29760  clwwlkvbij  30061  splfv3  32909  ballotlemimin  34490  ballotlemsdom  34496  ballotlemsel1i  34497  ballotlemsima  34500  ballotlemfrc  34511  ballotlemfrceq  34513  fzssfzo  34523  fsum2dsub  34591  pfxwlk  35117  erdszelem7  35190  erdszelem8  35191  elfzm12  35668  poimirlem1  37621  poimirlem2  37622  poimirlem4  37624  poimirlem6  37626  poimirlem7  37627  poimirlem9  37629  poimirlem15  37635  poimirlem16  37636  poimirlem17  37637  poimirlem19  37639  poimirlem22  37642  poimirlem23  37643  poimirlem24  37644  poimirlem26  37646  poimirlem27  37647  poimirlem28  37648  poimirlem31  37651  mettrifi  37757  eldiophb  42750  eldioph2lem2  42754  diophrex  42768  fmul01  45581  fmulcl  45582  dvnprodlem2  45948  stoweidlem11  46012  stoweidlem17  46018  stoweidlem26  46027  iccpartres  47422  iccpartipre  47425