| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fsumsub | Structured version Visualization version GIF version | ||
| Description: Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
| Ref | Expression |
|---|---|
| fsumneg.1 | ⊢ (𝜑 → 𝐴 ∈ Fin) |
| fsumneg.2 | ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| fsumsub.3 | ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| Ref | Expression |
|---|---|
| fsumsub | ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fsumneg.1 | . . . 4 ⊢ (𝜑 → 𝐴 ∈ Fin) | |
| 2 | fsumneg.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | |
| 3 | fsumsub.3 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) | |
| 4 | 3 | negcld 11496 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -𝐶 ∈ ℂ) |
| 5 | 1, 2, 4 | fsumadd 15682 | . . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + -𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 -𝐶)) |
| 6 | 1, 3 | fsumneg 15729 | . . . 4 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -𝐶 = -Σ𝑘 ∈ 𝐴 𝐶) |
| 7 | 6 | oveq2d 7385 | . . 3 ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 -𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + -Σ𝑘 ∈ 𝐴 𝐶)) |
| 8 | 5, 7 | eqtrd 2764 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + -𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + -Σ𝑘 ∈ 𝐴 𝐶)) |
| 9 | 2, 3 | negsubd 11515 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 + -𝐶) = (𝐵 − 𝐶)) |
| 10 | 9 | sumeq2dv 15644 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + -𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶)) |
| 11 | 1, 2 | fsumcl 15675 | . . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
| 12 | 1, 3 | fsumcl 15675 | . . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
| 13 | 11, 12 | negsubd 11515 | . 2 ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 + -Σ𝑘 ∈ 𝐴 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶)) |
| 14 | 8, 10, 13 | 3eqtr3d 2772 | 1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 (class class class)co 7369 Fincfn 8895 ℂcc 11042 + caddc 11047 − cmin 11381 -cneg 11382 Σcsu 15628 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-rp 12928 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629 |
| This theorem is referenced by: fsumle 15741 fsumlt 15742 telfsumo 15744 fsumparts 15748 mertens 15828 bpolydiflem 15996 3dvds 16277 pcfac 16846 pcbc 16847 ramcl 16976 ovolicc2lem4 25397 dvfsumabs 25905 coeeulem 26105 birthdaylem2 26838 emcllem5 26886 lgamcvg2 26941 chpub 27107 logfaclbnd 27109 lgsquadlem1 27267 vmadivsum 27369 rpvmasumlem 27374 dchrmusum2 27381 dchrvmasumiflem2 27389 rpvmasum2 27399 dchrisum0lem2a 27404 dchrisum0lem2 27405 rplogsum 27414 mulogsumlem 27418 mulogsum 27419 mulog2sumlem1 27421 mulog2sumlem2 27422 mulog2sumlem3 27423 vmalogdivsum2 27425 vmalogdivsum 27426 2vmadivsumlem 27427 logsqvma 27429 selberglem1 27432 selberg3lem1 27444 selberg4lem1 27447 pntrsumo1 27452 selbergr 27455 selberg3r 27456 selberg4r 27457 selberg34r 27458 pntrlog2bndlem4 27467 pntrlog2bndlem5 27468 pntlemo 27494 ax5seglem9 28840 fwddifnp1 36126 knoppndvlem11 36483 sticksstones10 42116 sticksstones12a 42118 oddnumth 42272 etransclem46 46251 |
| Copyright terms: Public domain | W3C validator |