| 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 13564 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾)) | |
| 2 | id 23 | . . . . 5 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ (ℤ≥‘𝑀)) | |
| 3 | uztrn 12896 | . . . . 5 ⊢ ((𝑘 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) | |
| 4 | 1, 2, 3 | syl2anr 609 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 5 | elfzuz3 13565 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘𝑘)) | |
| 6 | 5 | adantl 487 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
| 7 | elfzuzb 13562 | . . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘))) | |
| 8 | 4, 6, 7 | sylanbrc 595 | . . 3 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
| 9 | 8 | ex 418 | . 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (𝑀...𝑁))) |
| 10 | 9 | ssrdv 3944 | 1 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∈ wcel 2146 ⊆ wss 3906 ‘cfv 6540 (class class class)co 7419 ℤ≥cuz 12878 ...cfz 13551 |
| 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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11171 ax-resscn 11172 ax-pre-lttri 11189 ax-pre-lttrn 11190 |
| 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 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-1st 7992 df-2nd 7993 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-neg 11459 df-z 12607 df-uz 12879 df-fz 13552 |
| This theorem is used by: fzssnn 13613 fzp1ss 13620 fzdif1 13650 ige2m1fz 13662 fzoss1 13732 fzossnn0 13736 sermono 14088 seqsplit 14089 seqf1olem2 14096 seqz 14104 seqcoll2 14520 swrdswrd 14764 swrdccatin2 14788 pfxccatin12lem2c 14789 pfxccatpfx2 14796 swrds2m 15002 mertenslem1 15961 reumodprminv 16886 prmgaplcmlem1 17133 structfn 17238 strleun 17239 cpmadugsumlemF 23083 ply1termlem 26411 dvply1 26496 ppisval2 27320 ppiltx 27392 chtlepsi 27421 chtublem 27426 chpub 27435 gausslemma2dlem3 27583 2lgslem1a 27606 chtppilimlem1 27688 pntlemq 27816 pntlemf 27820 axlowdimlem16 29362 axlowdimlem17 29363 axlowdim 29366 cyclnumvtx 30215 crctcshwlkn0lem3 30228 swrdrndisj 33341 esumpmono 34533 ballotlem2 34944 ballotlemfc0 34948 ballotlemfcc 34949 fsum2dsub 35059 chtvalz 35081 poimirlem1 38329 poimirlem2 38330 poimirlem4 38332 poimirlem6 38334 poimirlem7 38335 poimirlem15 38343 poimirlem16 38344 poimirlem19 38347 poimirlem20 38348 poimirlem23 38351 poimirlem27 38355 fdc 38454 jm2.23 43781 stoweidlem11 46783 elaa2lem 47005 elfz2nn 48117 iccpartgel 48236 |
| Copyright terms: Public domain | W3C validator |