Theorem fzss2 13583

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 13539	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	adantl 486	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀))
3		elfzuz3 13540	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘))
4		uztrn 12871	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘))
5	3, 4	sylan2 604	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘))
6		elfzuzb 13537	. . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘)))
7	2, 5, 6	sylanbrc 594	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
8	7	ex 417	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
9	8	ssrdv 3945	1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   ⊆ wss 3907  ‘cfv 6525  (class class class)co 7400  ℤ_≥cuz 12853  ...cfz 13526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-pre-lttri 11162  ax-pre-lttrn 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-neg 11432  df-z 12583  df-uz 12854  df-fz 13527

This theorem is referenced by:  fzssp1  13586  elfz0add  13645  predfz  13672  fzoss2  13707  sermono  14061  seqsplit  14062  seqcaopr2  14065  seqf1olem2a  14067  seqf1olem2  14069  seqhomo  14076  seqz  14077  bcm1k  14342  seqcoll  14491  seqcoll2  14492  isercoll  15709  fsum0diaglem  15817  fsum0diag2  15824  cvgcmpce  15860  mertenslem1  15928  prodfn0  15938  prodfrec  15939  binomfallfaclem2  16084  bpoly4  16103  prmdvdsbc  16775  eulerthlem2  16831  pcfac  16949  vdwnnlem2  17046  strleun  17207  gsumzaddlem  19982  telgsumfzs  20050  freshmansdream  21684  imasdsf1olem  24491  plyaddlem1  26331  plymullem1  26332  coeeulem  26342  coeidlem  26355  coeid3  26358  coefv0  26366  coemulc  26373  vieta1lem2  26433  ppinprm  27274  chtnprm  27276  chpwordi  27279  chtublem  27333  bposlem1  27406  gausslemma2dlem2  27489  lgsquadlem3  27504  chebbnd1lem1  27591  vmadivsumb  27605  dchrvmasumiflem1  27623  mulog2sumlem2  27657  selbergb  27671  selberg2b  27674  chpdifbndlem1  27675  logdivbnd  27678  selberg3lem2  27680  pntrsumbnd  27688  pntlemq  27723  axlowdimlem16  29216  axlowdimlem17  29217  wlkres  29927  crctcshwlkn0lem2  30069  clwwlkvbij  30373  splfv3  33191  ballotlemimin  34813  ballotlemsdom  34819  ballotlemsel1i  34820  ballotlemsima  34823  ballotlemfrc  34834  ballotlemfrceq  34836  fzssfzo  34846  fsum2dsub  34911  pfxwlk  35487  erdszelem7  35560  erdszelem8  35561  elfzm12  36038  poimirlem1  38132  poimirlem2  38133  poimirlem4  38135  poimirlem6  38137  poimirlem7  38138  poimirlem9  38140  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  poimirlem31  38162  mettrifi  38268  eldiophb  43350  eldioph2lem2  43354  diophrex  43368  fmul01  46154  fmulcl  46155  dvnprodlem2  46519  stoweidlem11  46583  stoweidlem17  46589  stoweidlem26  46598  iccpartres  48022  iccpartipre  48025