![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fsumser | Structured version Visualization version GIF version |
Description: A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition of follows as fsum1 14646 and fsump1i 14670, which should make our notation clear and from which, along with closure fsumcl 14634, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) |
Ref | Expression |
---|---|
fsumser.1 | ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴) |
fsumser.2 | ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
fsumser.3 | ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
fsumser | ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( + , 𝐹)‘𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2815 | . . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑚 ∈ (𝑀...𝑁) ↔ 𝑘 ∈ (𝑀...𝑁))) | |
2 | fveq2 6340 | . . . . . 6 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) | |
3 | 1, 2 | ifbieq1d 4241 | . . . . 5 ⊢ (𝑚 = 𝑘 → if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0) = if(𝑘 ∈ (𝑀...𝑁), (𝐹‘𝑘), 0)) |
4 | eqid 2748 | . . . . 5 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0)) = (𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0)) | |
5 | fvex 6350 | . . . . . 6 ⊢ (𝐹‘𝑘) ∈ V | |
6 | c0ex 10197 | . . . . . 6 ⊢ 0 ∈ V | |
7 | 5, 6 | ifex 4288 | . . . . 5 ⊢ if(𝑘 ∈ (𝑀...𝑁), (𝐹‘𝑘), 0) ∈ V |
8 | 3, 4, 7 | fvmpt 6432 | . . . 4 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0))‘𝑘) = if(𝑘 ∈ (𝑀...𝑁), (𝐹‘𝑘), 0)) |
9 | fsumser.1 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴) | |
10 | 9 | ifeq1da 4248 | . . . 4 ⊢ (𝜑 → if(𝑘 ∈ (𝑀...𝑁), (𝐹‘𝑘), 0) = if(𝑘 ∈ (𝑀...𝑁), 𝐴, 0)) |
11 | 8, 10 | sylan9eqr 2804 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0))‘𝑘) = if(𝑘 ∈ (𝑀...𝑁), 𝐴, 0)) |
12 | fsumser.2 | . . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | |
13 | fsumser.3 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) | |
14 | ssid 3753 | . . . 4 ⊢ (𝑀...𝑁) ⊆ (𝑀...𝑁) | |
15 | 14 | a1i 11 | . . 3 ⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀...𝑁)) |
16 | 11, 12, 13, 15 | fsumsers 14629 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( + , (𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0)))‘𝑁)) |
17 | elfzuz 12502 | . . . . . 6 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) | |
18 | 17, 8 | syl 17 | . . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0))‘𝑘) = if(𝑘 ∈ (𝑀...𝑁), (𝐹‘𝑘), 0)) |
19 | iftrue 4224 | . . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → if(𝑘 ∈ (𝑀...𝑁), (𝐹‘𝑘), 0) = (𝐹‘𝑘)) | |
20 | 18, 19 | eqtrd 2782 | . . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0))‘𝑘) = (𝐹‘𝑘)) |
21 | 20 | adantl 473 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0))‘𝑘) = (𝐹‘𝑘)) |
22 | 12, 21 | seqfveq 12990 | . 2 ⊢ (𝜑 → (seq𝑀( + , (𝑚 ∈ (ℤ≥‘𝑀) ↦ if(𝑚 ∈ (𝑀...𝑁), (𝐹‘𝑚), 0)))‘𝑁) = (seq𝑀( + , 𝐹)‘𝑁)) |
23 | 16, 22 | eqtrd 2782 | 1 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( + , 𝐹)‘𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1620 ∈ wcel 2127 ⊆ wss 3703 ifcif 4218 ↦ cmpt 4869 ‘cfv 6037 (class class class)co 6801 ℂcc 10097 0cc0 10099 + caddc 10102 ℤ≥cuz 11850 ...cfz 12490 seqcseq 12966 Σcsu 14586 |
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-rep 4911 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-inf2 8699 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176 ax-pre-sup 10177 |
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-reu 3045 df-rmo 3046 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-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-int 4616 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-se 5214 df-we 5215 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-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 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-isom 6046 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-om 7219 df-1st 7321 df-2nd 7322 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-1o 7717 df-oadd 7721 df-er 7899 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-sup 8501 df-oi 8568 df-card 8926 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-div 10848 df-nn 11184 df-2 11242 df-3 11243 df-n0 11456 df-z 11541 df-uz 11851 df-rp 11997 df-fz 12491 df-fzo 12631 df-seq 12967 df-exp 13026 df-hash 13283 df-cj 14009 df-re 14010 df-im 14011 df-sqrt 14145 df-abs 14146 df-clim 14389 df-sum 14587 |
This theorem is referenced by: isumclim3 14660 seqabs 14716 cvgcmpce 14720 isumsplit 14742 climcndslem1 14751 climcndslem2 14752 climcnds 14753 trireciplem 14764 geolim 14771 geo2lim 14776 mertenslem2 14787 mertens 14788 efcvgfsum 14986 effsumlt 15011 prmreclem6 15798 prmrec 15799 ovollb2lem 23427 ovoliunlem1 23441 ovoliun2 23445 ovolscalem1 23452 ovolicc2lem4 23459 uniioovol 23518 uniioombllem3 23524 uniioombllem6 23527 mtest 24328 mtestbdd 24329 psercn2 24347 pserdvlem2 24352 abelthlem6 24360 logfac 24517 emcllem5 24896 lgamcvg2 24951 basellem8 24984 prmorcht 25074 pclogsum 25110 dchrisumlem2 25349 dchrmusum2 25353 dchrvmasumiflem1 25360 dchrisum0re 25372 dchrisum0lem1b 25374 dchrisum0lem2a 25376 dchrisum0lem2 25377 esumpcvgval 30420 esumcvg 30428 esumcvgsum 30430 knoppcnlem11 32770 fsumsermpt 40283 sumnnodd 40334 fourierdlem112 40907 sge0isum 41116 sge0seq 41135 |
Copyright terms: Public domain | W3C validator |