![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzoss2 | Structured version Visualization version GIF version |
Description: Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
Ref | Expression |
---|---|
fzoss2 | ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀..^𝐾) ⊆ (𝑀..^𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluzel2 12063 | . . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ∈ ℤ) | |
2 | peano2zm 11838 | . . . . 5 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ) | |
3 | 1, 2 | syl 17 | . . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝐾 − 1) ∈ ℤ) |
4 | 1zzd 11826 | . . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 1 ∈ ℤ) | |
5 | id 22 | . . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ (ℤ≥‘𝐾)) | |
6 | 1 | zcnd 11901 | . . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ∈ ℂ) |
7 | ax-1cn 10393 | . . . . . . 7 ⊢ 1 ∈ ℂ | |
8 | npcan 10696 | . . . . . . 7 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾) | |
9 | 6, 7, 8 | sylancl 577 | . . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → ((𝐾 − 1) + 1) = 𝐾) |
10 | 9 | fveq2d 6503 | . . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (ℤ≥‘((𝐾 − 1) + 1)) = (ℤ≥‘𝐾)) |
11 | 5, 10 | eleqtrrd 2869 | . . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ (ℤ≥‘((𝐾 − 1) + 1))) |
12 | eluzsub 12088 | . . . 4 ⊢ (((𝐾 − 1) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘((𝐾 − 1) + 1))) → (𝑁 − 1) ∈ (ℤ≥‘(𝐾 − 1))) | |
13 | 3, 4, 11, 12 | syl3anc 1351 | . . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑁 − 1) ∈ (ℤ≥‘(𝐾 − 1))) |
14 | fzss2 12763 | . . 3 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 − 1))) | |
15 | 13, 14 | syl 17 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 − 1))) |
16 | fzoval 12855 | . . 3 ⊢ (𝐾 ∈ ℤ → (𝑀..^𝐾) = (𝑀...(𝐾 − 1))) | |
17 | 1, 16 | syl 17 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀..^𝐾) = (𝑀...(𝐾 − 1))) |
18 | eluzelz 12068 | . . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ ℤ) | |
19 | fzoval 12855 | . . 3 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) | |
20 | 18, 19 | syl 17 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
21 | 15, 17, 20 | 3sstr4d 3904 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀..^𝐾) ⊆ (𝑀..^𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ⊆ wss 3829 ‘cfv 6188 (class class class)co 6976 ℂcc 10333 1c1 10336 + caddc 10338 − cmin 10670 ℤcz 11793 ℤ≥cuz 12058 ...cfz 12708 ..^cfzo 12849 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-om 7397 df-1st 7501 df-2nd 7502 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-nn 11440 df-n0 11708 df-z 11794 df-uz 12059 df-fz 12709 df-fzo 12850 |
This theorem is referenced by: fzossrbm1 12881 fzosplit 12885 elfzoext 12909 fzossfzop1 12930 uzindi 13165 ccatass 13751 ccatrn 13752 ccatalpha 13756 swrdval2 13809 swrd0valOLD 13810 swrd0lenOLD 13811 swrdccat1OLD 13850 pfxres 13861 pfxf 13862 pfxccat1 13884 swrdccatin12lem2a 13926 splfv1 13971 splfv1OLD 13972 revccat 13985 repswpfx 14004 psgnunilem5 18383 psgnunilem5OLD 18384 efgsp1 18621 efgsres 18622 efgsresOLD 18623 wlkres 27156 wlkresOLD 27158 trlreslem 27187 trlreslemOLD 27189 crctcshwlkn0lem4 27299 wwlksm1edg 27367 wwlksm1edgOLD 27368 wwlksnred 27379 wwlksnredOLD 27380 clwwlkccatlem 27495 clwlkclwwlklem2fv1 27501 clwlkclwwlklem2 27506 clwwisshclwwslem 27529 clwwlkinwwlk 27555 clwwlkinwwlkOLD 27556 clwwlkfOLD 27564 clwwlkf 27569 wwlksubclwwlk 27581 wwlksubclwwlkOLD 27582 trlsegvdeg 27757 iundisjfi 30275 fz1nntr 30281 wrdres 30366 measiuns 31127 signstfvp 31494 signstfvc 31497 signstres 31498 signsvfn 31506 prodfzo03 31528 breprexplemc 31557 iccpartres 42956 iccpartigtl 42961 iccelpart 42971 |
Copyright terms: Public domain | W3C validator |