| 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 13552 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾)) | |
| 2 | id 23 | . . . . 5 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ (ℤ≥‘𝑀)) | |
| 3 | uztrn 12884 | . . . . 5 ⊢ ((𝑘 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) | |
| 4 | 1, 2, 3 | syl2anr 608 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 5 | elfzuz3 13553 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘𝑘)) | |
| 6 | 5 | adantl 486 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
| 7 | elfzuzb 13550 | . . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘))) | |
| 8 | 4, 6, 7 | sylanbrc 594 | . . 3 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
| 9 | 8 | ex 417 | . 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (𝑀...𝑁))) |
| 10 | 9 | ssrdv 3943 | 1 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∈ wcel 2143 ⊆ wss 3905 ‘cfv 6536 (class class class)co 7410 ℤ≥cuz 12866 ...cfz 13539 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11160 ax-resscn 11161 ax-pre-lttri 11178 ax-pre-lttrn 11179 |
| This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7982 df-2nd 7983 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-neg 11448 df-z 12596 df-uz 12867 df-fz 13540 |
| This theorem is used by: fzssnn 13601 fzp1ss 13608 fzdif1 13638 ige2m1fz 13650 fzoss1 13720 fzossnn0 13724 sermono 14075 seqsplit 14076 seqf1olem2 14083 seqz 14091 seqcoll2 14507 swrdswrd 14747 swrdccatin2 14771 pfxccatin12lem2c 14772 pfxccatpfx2 14779 swrds2m 14983 mertenslem1 15943 reumodprminv 16868 prmgaplcmlem1 17115 structfn 17220 strleun 17221 cpmadugsumlemF 23042 ply1termlem 26369 dvply1 26454 ppisval2 27278 ppiltx 27350 chtlepsi 27379 chtublem 27384 chpub 27393 gausslemma2dlem3 27541 2lgslem1a 27564 chtppilimlem1 27646 pntlemq 27774 pntlemf 27778 axlowdimlem16 29316 axlowdimlem17 29317 axlowdim 29320 cyclnumvtx 30158 crctcshwlkn0lem3 30170 swrdrndisj 33286 esumpmono 34478 ballotlem2 34888 ballotlemfc0 34892 ballotlemfcc 34893 fsum2dsub 35003 chtvalz 35025 poimirlem1 38300 poimirlem2 38301 poimirlem4 38303 poimirlem6 38305 poimirlem7 38306 poimirlem15 38314 poimirlem16 38315 poimirlem19 38318 poimirlem20 38319 poimirlem23 38322 poimirlem27 38326 fdc 38424 jm2.23 43751 stoweidlem11 46753 elaa2lem 46975 elfz2nn 48087 iccpartgel 48206 |
| Copyright terms: Public domain | W3C validator |