![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > seqcl | Structured version Visualization version GIF version |
Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
Ref | Expression |
---|---|
seqcl.1 | ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
seqcl.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
seqcl.3 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
Ref | Expression |
---|---|
seqcl | ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6541 | . . . 4 ⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) | |
2 | 1 | eleq1d 2866 | . . 3 ⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑀) ∈ 𝑆)) |
3 | seqcl.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) | |
4 | 3 | ralrimiva 3148 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ 𝑆) |
5 | seqcl.1 | . . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | |
6 | eluzfz1 12764 | . . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) | |
7 | 5, 6 | syl 17 | . . 3 ⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
8 | 2, 4, 7 | rspcdva 3563 | . 2 ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆) |
9 | seqcl.3 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) | |
10 | eluzel2 12098 | . . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | |
11 | 5, 10 | syl 17 | . . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | fzp1ss 12808 | . . . . 5 ⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) | |
13 | 11, 12 | syl 17 | . . . 4 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
14 | 13 | sselda 3891 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
15 | 14, 3 | syldan 591 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
16 | 8, 9, 5, 15 | seqcl2 13238 | 1 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 ⊆ wss 3861 ‘cfv 6228 (class class class)co 7019 1c1 10387 + caddc 10389 ℤcz 11831 ℤ≥cuz 12093 ...cfz 12742 seqcseq 13219 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-cnex 10442 ax-resscn 10443 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-mulcom 10450 ax-addass 10451 ax-mulass 10452 ax-distr 10453 ax-i2m1 10454 ax-1ne0 10455 ax-1rid 10456 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 ax-pre-lttri 10460 ax-pre-lttrn 10461 ax-pre-ltadd 10462 ax-pre-mulgt0 10463 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-reu 3111 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-pss 3878 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-tp 4479 df-op 4481 df-uni 4748 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-tr 5067 df-id 5351 df-eprel 5356 df-po 5365 df-so 5366 df-fr 5405 df-we 5407 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-pred 6026 df-ord 6072 df-on 6073 df-lim 6074 df-suc 6075 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-om 7440 df-1st 7548 df-2nd 7549 df-wrecs 7801 df-recs 7863 df-rdg 7901 df-er 8142 df-en 8361 df-dom 8362 df-sdom 8363 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-sub 10721 df-neg 10722 df-nn 11489 df-n0 11748 df-z 11832 df-uz 12094 df-fz 12743 df-seq 13220 |
This theorem is referenced by: sermono 13252 seqsplit 13253 seqcaopr2 13256 seqf1olem2a 13258 seqf1olem2 13260 seqid3 13264 seqhomo 13267 seqz 13268 seqdistr 13271 serge0 13274 serle 13275 seqof 13277 seqcoll 13670 seqcoll2 13671 fsumcl2lem 14921 prodfn0 15083 prodfrec 15084 prodfdiv 15085 fprodcl2lem 15137 eulerthlem2 15948 gsumwsubmcl 17814 mulgnnsubcl 17995 gsumzcl2 18751 gsumzaddlem 18761 gsummptfzcl 18809 lgscllem 25562 lgsval4a 25577 lgsneg 25579 lgsdir 25590 lgsdilem2 25591 lgsdi 25592 lgsne0 25593 gsumncl 31419 faclim 32580 knoppcnlem8 33442 mblfinlem2 34474 fmul01 41416 fmulcl 41417 fmuldfeq 41419 fmul01lt1lem1 41420 fmul01lt1lem2 41421 stoweidlem3 41844 stoweidlem42 41883 stoweidlem48 41889 wallispilem4 41909 wallispi 41911 wallispi2lem1 41912 wallispi2 41914 stirlinglem5 41919 stirlinglem7 41921 stirlinglem10 41924 sge0isum 42265 |
Copyright terms: Public domain | W3C validator |