Theorem fzss2 13728

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900  ‘cfv 6561  (class class class)co 7446  ℤ_≥cuz 12995  ...cfz 13669

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-pre-lttri 11304  ax-pre-lttrn 11305

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-oprab 7450  df-mpo 7451  df-1st 8028  df-2nd 8029  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-neg 11574  df-z 12724  df-uz 12996  df-fz 13670

This theorem is used by:  fzssp1  13731  elfz0add  13790  predfz  13817  fzoss2  13852  sermono  14207  seqsplit  14208  seqcaopr2  14211  seqf1olem2a  14213  seqf1olem2  14215  seqhomo  14222  seqz  14223  bcm1k  14489  seqcoll  14639  seqcoll2  14640  isercoll  15867  fsum0diaglem  15974  fsum0diag2  15981  cvgcmpce  16017  mertenslem1  16085  prodfn0  16095  prodfrec  16096  binomfallfaclem2  16238  bpoly4  16257  prmdvdsbc  16934  eulerthlem2  16991  pcfac  17109  vdwnnlem2  17206  strleun  17367  gsumzaddlem  20168  telgsumfzs  20236  freshmansdream  21913  imasdsf1olem  24725  plyaddlem1  26565  plymullem1  26566  coeeulem  26576  coeidlem  26589  coeid3  26592  coefv0  26600  coemulc  26607  vieta1lem2  26667  ppinprm  27512  chtnprm  27514  chpwordi  27517  chtublem  27571  bposlem1  27644  gausslemma2dlem2  27727  lgsquadlem3  27742  chebbnd1lem1  27829  vmadivsumb  27843  dchrvmasumiflem1  27861  mulog2sumlem2  27895  selbergb  27909  selberg2b  27912  chpdifbndlem1  27913  logdivbnd  27916  selberg3lem2  27918  pntrsumbnd  27926  pntlemq  27961  axlowdimlem16  29568  axlowdimlem17  29569  wlkres  30282  pfxwlk  30299  crctcshwlkn0lem2  30433  clwwlkvbij  30737  splfv3  33592  ballotlemimin  35221  ballotlemsdom  35227  ballotlemsel1i  35228  ballotlemsima  35231  ballotlemfrc  35242  ballotlemfrceq  35244  fzssfzo  35254  fsum2dsub  35319  erdszelem7  36142  erdszelem8  36143  elfzm12  36620  poimirlem1  38744  poimirlem2  38745  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem9  38752  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem26  38769  poimirlem27  38770  poimirlem28  38771  poimirlem31  38774  mettrifi  38894  eldiophb  43972  eldioph2lem2  43976  diophrex  43990  fmul01  46807  fmulcl  46808  dvnprodlem2  47172  stoweidlem11  47236  stoweidlem17  47242  stoweidlem26  47251  iccpartres  48715  iccpartipre  48718