![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzss1 | Structured version Visualization version GIF version |
Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
fzss1 | ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz 12502 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾)) | |
2 | id 22 | . . . . 5 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ (ℤ≥‘𝑀)) | |
3 | uztrn 11867 | . . . . 5 ⊢ ((𝑘 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) | |
4 | 1, 2, 3 | syl2anr 496 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
5 | elfzuz3 12503 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘𝑘)) | |
6 | 5 | adantl 473 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
7 | elfzuzb 12500 | . . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘))) | |
8 | 4, 6, 7 | sylanbrc 701 | . . 3 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
9 | 8 | ex 449 | . 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (𝑀...𝑁))) |
10 | 9 | ssrdv 3738 | 1 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2127 ⊆ wss 3703 ‘cfv 6037 (class class class)co 6801 ℤ≥cuz 11850 ...cfz 12490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-pre-lttri 10173 ax-pre-lttrn 10174 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-id 5162 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-1st 7321 df-2nd 7322 df-er 7899 df-en 8110 df-dom 8111 df-sdom 8112 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-neg 10432 df-z 11541 df-uz 11851 df-fz 12491 |
This theorem is referenced by: fzssnn 12549 fzp1ss 12556 ige2m1fz 12594 fzoss1 12660 fzossnn0 12664 sermono 12998 seqsplit 12999 seqf1olem2 13006 seqz 13014 seqcoll2 13412 swrdswrd 13631 swrdccatin2 13658 swrdccatin12lem2c 13659 swrdccatin12 13662 swrds2m 13857 mertenslem1 14786 reumodprminv 15682 prmgaplcmlem1 15928 structfn 16047 strleun 16145 cpmadugsumlemF 20854 ply1termlem 24129 dvply1 24209 ppisval2 25001 ppiltx 25073 chtlepsi 25101 chtublem 25106 chpub 25115 gausslemma2dlem3 25263 2lgslem1a 25286 chtppilimlem1 25332 pntlemq 25460 pntlemf 25464 axlowdimlem16 26007 axlowdimlem17 26008 axlowdim 26011 crctcshwlkn0lem3 26886 esumpmono 30421 ballotlem2 30830 ballotlemfc0 30834 ballotlemfcc 30835 fsum2dsub 30965 chtvalz 30987 poimirlem1 33692 poimirlem2 33693 poimirlem4 33695 poimirlem6 33697 poimirlem7 33698 poimirlem15 33706 poimirlem16 33707 poimirlem19 33710 poimirlem20 33711 poimirlem23 33714 poimirlem27 33718 fdc 33823 jm2.23 38034 stoweidlem11 40700 elaa2lem 40922 iccpartgel 41844 pfxccatin12 41904 pfxccatpfx2 41907 |
Copyright terms: Public domain | W3C validator |