MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fzss2 Structured version   Visualization version   GIF version

Theorem fzss2 13595
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.
StepHypRef Expression
1 elfzuz 13551 . . . . 5 (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ𝑀))
21adantl 480 . . . 4 ((𝑁 ∈ (ℤ𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ𝑀))
3 elfzuz3 13552 . . . . 5 (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ𝑘))
4 uztrn 12892 . . . . 5 ((𝑁 ∈ (ℤ𝐾) ∧ 𝐾 ∈ (ℤ𝑘)) → 𝑁 ∈ (ℤ𝑘))
53, 4sylan2 591 . . . 4 ((𝑁 ∈ (ℤ𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ𝑘))
6 elfzuzb 13549 . . . 4 (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑘)))
72, 5, 6sylanbrc 581 . . 3 ((𝑁 ∈ (ℤ𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁))
87ex 411 . 2 (𝑁 ∈ (ℤ𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁)))
98ssrdv 3985 1 (𝑁 ∈ (ℤ𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2099  wss 3947  cfv 6554  (class class class)co 7424  cuz 12874  ...cfz 13538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-pre-lttri 11232  ax-pre-lttrn 11233
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8003  df-2nd 8004  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-neg 11497  df-z 12611  df-uz 12875  df-fz 13539
This theorem is referenced by:  fzssp1  13598  elfz0add  13654  predfz  13680  fzoss2  13714  sermono  14054  seqsplit  14055  seqcaopr2  14058  seqf1olem2a  14060  seqf1olem2  14062  seqhomo  14069  seqz  14070  bcm1k  14332  seqcoll  14483  seqcoll2  14484  isercoll  15672  fsum0diaglem  15780  fsum0diag2  15787  cvgcmpce  15822  mertenslem1  15888  prodfn0  15898  prodfrec  15899  binomfallfaclem2  16042  bpoly4  16061  prmdvdsbc  16728  eulerthlem2  16784  pcfac  16901  vdwnnlem2  16998  strleun  17159  gsumzaddlem  19919  telgsumfzs  19987  freshmansdream  21572  imasdsf1olem  24370  plyaddlem1  26240  plymullem1  26241  coeeulem  26251  coeidlem  26264  coeid3  26267  coefv0  26275  coemulc  26282  vieta1lem2  26339  ppinprm  27180  chtnprm  27182  chpwordi  27185  chtublem  27240  bposlem1  27313  gausslemma2dlem2  27396  lgsquadlem3  27411  chebbnd1lem1  27498  vmadivsumb  27512  dchrvmasumiflem1  27530  mulog2sumlem2  27564  selbergb  27578  selberg2b  27581  chpdifbndlem1  27582  logdivbnd  27585  selberg3lem2  27587  pntrsumbnd  27595  pntlemq  27630  axlowdimlem16  28891  axlowdimlem17  28892  wlkres  29607  crctcshwlkn0lem2  29745  clwwlkvbij  30046  splfv3  32822  ballotlemimin  34339  ballotlemsdom  34345  ballotlemsel1i  34346  ballotlemsima  34349  ballotlemfrc  34360  ballotlemfrceq  34362  fzssfzo  34385  fsum2dsub  34453  pfxwlk  34951  erdszelem7  35025  erdszelem8  35026  elfzm12  35503  poimirlem1  37322  poimirlem2  37323  poimirlem4  37325  poimirlem6  37327  poimirlem7  37328  poimirlem9  37330  poimirlem15  37336  poimirlem16  37337  poimirlem17  37338  poimirlem19  37340  poimirlem22  37343  poimirlem23  37344  poimirlem24  37345  poimirlem26  37347  poimirlem27  37348  poimirlem28  37349  poimirlem31  37352  mettrifi  37458  eldiophb  42414  eldioph2lem2  42418  diophrex  42432  fmul01  45201  fmulcl  45202  dvnprodlem2  45568  stoweidlem11  45632  stoweidlem17  45638  stoweidlem26  45647  iccpartres  46990  iccpartipre  46993
  Copyright terms: Public domain W3C validator