MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fzss1 Structured version   Unicode version

Theorem fzss1 11488
Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
fzss1  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K ... N )  C_  ( M ... N ) )

Proof of Theorem fzss1
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 elfzuz 11440 . . . . 5  |-  ( k  e.  ( K ... N )  ->  k  e.  ( ZZ>= `  K )
)
2 id 22 . . . . 5  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ( ZZ>= `  M )
)
3 uztrn 10869 . . . . 5  |-  ( ( k  e.  ( ZZ>= `  K )  /\  K  e.  ( ZZ>= `  M )
)  ->  k  e.  ( ZZ>= `  M )
)
41, 2, 3syl2anr 475 . . . 4  |-  ( ( K  e.  ( ZZ>= `  M )  /\  k  e.  ( K ... N
) )  ->  k  e.  ( ZZ>= `  M )
)
5 elfzuz3 11441 . . . . 5  |-  ( k  e.  ( K ... N )  ->  N  e.  ( ZZ>= `  k )
)
65adantl 463 . . . 4  |-  ( ( K  e.  ( ZZ>= `  M )  /\  k  e.  ( K ... N
) )  ->  N  e.  ( ZZ>= `  k )
)
7 elfzuzb 11438 . . . 4  |-  ( k  e.  ( M ... N )  <->  ( k  e.  ( ZZ>= `  M )  /\  N  e.  ( ZZ>=
`  k ) ) )
84, 6, 7sylanbrc 659 . . 3  |-  ( ( K  e.  ( ZZ>= `  M )  /\  k  e.  ( K ... N
) )  ->  k  e.  ( M ... N
) )
98ex 434 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( k  e.  ( K ... N
)  ->  k  e.  ( M ... N ) ) )
109ssrdv 3354 1  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K ... N )  C_  ( M ... N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1757    C_ wss 3320   ` cfv 5410  (class class class)co 6084   ZZ>=cuz 10853   ...cfz 11428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-cnex 9330  ax-resscn 9331  ax-pre-lttri 9348  ax-pre-lttrn 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-op 3876  df-uni 4084  df-iun 4165  df-br 4285  df-opab 4343  df-mpt 4344  df-id 4627  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6570  df-2nd 6571  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-neg 9590  df-z 10639  df-uz 10854  df-fz 11429
This theorem is referenced by:  fzp1ss  11495  fzoss1  11564  fzossnn0  11568  sermono  11826  seqsplit  11827  seqf1olem2  11834  seqz  11842  bcpasc  12085  seqcoll2  12205  swrd0fv0  12324  swrd0fvlsw  12327  swrdswrd  12342  swrdccatin2  12366  swrdccatin12lem2c  12367  swrdccatin12  12370  mertenslem1  13331  reumodprminv  13859  structfn  14174  strleun  14255  efgsres  16219  efgredlemd  16225  efgredlem  16228  ply1termlem  21560  dvply1  21639  dvtaylp  21724  taylthlem2  21728  basellem5  22311  ppisval2  22331  ppiltx  22404  chtlepsi  22434  chtublem  22439  chpub  22448  chtppilimlem1  22611  pntlemq  22739  pntlemf  22743  axlowdimlem16  23030  axlowdimlem17  23031  axlowdim  23034  fzssnn  25901  esumpmono  26386  ballotlem2  26723  ballotlemfc0  26727  ballotlemfcc  26728  ballotlemfrci  26762  ballotlemfrceq  26763  fdc  28489  jm2.23  29194  stoweidlem11  29656  ige2m1fz  30056  extwwlkfablem2  30521
  Copyright terms: Public domain W3C validator