![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fsumsplit | Structured version Visualization version GIF version |
Description: Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
Ref | Expression |
---|---|
fsumsplit.1 | ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
fsumsplit.2 | ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
fsumsplit.3 | ⊢ (𝜑 → 𝑈 ∈ Fin) |
fsumsplit.4 | ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
fsumsplit | ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 4064 | . . . . 5 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | |
2 | fsumsplit.2 | . . . . 5 ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) | |
3 | 1, 2 | sseqtrrid 3936 | . . . 4 ⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
4 | 3 | sselda 3884 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑈) |
5 | fsumsplit.4 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) | |
6 | 4, 5 | syldan 591 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
7 | 6 | ralrimiva 3147 | . . . 4 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
8 | fsumsplit.3 | . . . . 5 ⊢ (𝜑 → 𝑈 ∈ Fin) | |
9 | 8 | olcd 869 | . . . 4 ⊢ (𝜑 → (𝑈 ⊆ (ℤ≥‘0) ∨ 𝑈 ∈ Fin)) |
10 | sumss2 14904 | . . . 4 ⊢ (((𝐴 ⊆ 𝑈 ∧ ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) ∧ (𝑈 ⊆ (ℤ≥‘0) ∨ 𝑈 ∈ Fin)) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0)) | |
11 | 3, 7, 9, 10 | syl21anc 834 | . . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0)) |
12 | ssun2 4065 | . . . . 5 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) | |
13 | 12, 2 | sseqtrrid 3936 | . . . 4 ⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
14 | 13 | sselda 3884 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝑈) |
15 | 14, 5 | syldan 591 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
16 | 15 | ralrimiva 3147 | . . . 4 ⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
17 | sumss2 14904 | . . . 4 ⊢ (((𝐵 ⊆ 𝑈 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) ∧ (𝑈 ⊆ (ℤ≥‘0) ∨ 𝑈 ∈ Fin)) → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0)) | |
18 | 13, 16, 9, 17 | syl21anc 834 | . . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0)) |
19 | 11, 18 | oveq12d 7025 | . 2 ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0))) |
20 | 0cn 10468 | . . . 4 ⊢ 0 ∈ ℂ | |
21 | ifcl 4419 | . . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) | |
22 | 5, 20, 21 | sylancl 586 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) |
23 | ifcl 4419 | . . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) | |
24 | 5, 20, 23 | sylancl 586 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) |
25 | 8, 22, 24 | fsumadd 14917 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0))) |
26 | 2 | eleq2d 2866 | . . . . . 6 ⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵))) |
27 | elun 4041 | . . . . . 6 ⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) | |
28 | 26, 27 | syl6bb 288 | . . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))) |
29 | 28 | biimpa 477 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
30 | iftrue 4381 | . . . . . . . 8 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) | |
31 | 30 | adantl 482 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) |
32 | noel 4211 | . . . . . . . . . . 11 ⊢ ¬ 𝑘 ∈ ∅ | |
33 | elin 4085 | . . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) | |
34 | fsumsplit.1 | . . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) | |
35 | 34 | eleq2d 2866 | . . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ 𝑘 ∈ ∅)) |
36 | 33, 35 | syl5rbbr 287 | . . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ ∅ ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
37 | 32, 36 | mtbii 327 | . . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) |
38 | imnan 400 | . . . . . . . . . 10 ⊢ ((𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵) ↔ ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) | |
39 | 37, 38 | sylibr 235 | . . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵)) |
40 | 39 | imp 407 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) |
41 | 40 | iffalsed 4386 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 0) |
42 | 31, 41 | oveq12d 7025 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (𝐶 + 0)) |
43 | 6 | addid1d 10676 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 + 0) = 𝐶) |
44 | 42, 43 | eqtrd 2829 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
45 | 39 | con2d 136 | . . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴)) |
46 | 45 | imp 407 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 ∈ 𝐴) |
47 | 46 | iffalsed 4386 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 0) |
48 | iftrue 4381 | . . . . . . . 8 ⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶) | |
49 | 48 | adantl 482 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶) |
50 | 47, 49 | oveq12d 7025 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (0 + 𝐶)) |
51 | 15 | addid2d 10677 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (0 + 𝐶) = 𝐶) |
52 | 50, 51 | eqtrd 2829 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
53 | 44, 52 | jaodan 950 | . . . 4 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
54 | 29, 53 | syldan 591 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
55 | 54 | sumeq2dv 14881 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = Σ𝑘 ∈ 𝑈 𝐶) |
56 | 19, 25, 55 | 3eqtr2rd 2836 | 1 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 842 = wceq 1520 ∈ wcel 2079 ∀wral 3103 ∪ cun 3852 ∩ cin 3853 ⊆ wss 3854 ∅c0 4206 ifcif 4375 ‘cfv 6217 (class class class)co 7007 Fincfn 8347 ℂcc 10370 0cc0 10372 + caddc 10375 ℤ≥cuz 12082 Σcsu 14864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-inf2 8939 ax-cnex 10428 ax-resscn 10429 ax-1cn 10430 ax-icn 10431 ax-addcl 10432 ax-addrcl 10433 ax-mulcl 10434 ax-mulrcl 10435 ax-mulcom 10436 ax-addass 10437 ax-mulass 10438 ax-distr 10439 ax-i2m1 10440 ax-1ne0 10441 ax-1rid 10442 ax-rnegex 10443 ax-rrecex 10444 ax-cnre 10445 ax-pre-lttri 10446 ax-pre-lttrn 10447 ax-pre-ltadd 10448 ax-pre-mulgt0 10449 ax-pre-sup 10450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-fal 1533 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-int 4777 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-se 5395 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-isom 6226 df-riota 6968 df-ov 7010 df-oprab 7011 df-mpo 7012 df-om 7428 df-1st 7536 df-2nd 7537 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-1o 7944 df-oadd 7948 df-er 8130 df-en 8348 df-dom 8349 df-sdom 8350 df-fin 8351 df-sup 8742 df-oi 8810 df-card 9203 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 df-le 10516 df-sub 10708 df-neg 10709 df-div 11135 df-nn 11476 df-2 11537 df-3 11538 df-n0 11735 df-z 11819 df-uz 12083 df-rp 12229 df-fz 12732 df-fzo 12873 df-seq 13208 df-exp 13268 df-hash 13529 df-cj 14280 df-re 14281 df-im 14282 df-sqrt 14416 df-abs 14417 df-clim 14667 df-sum 14865 |
This theorem is referenced by: fsumsplitf 14919 sumpr 14924 sumtp 14925 fsumm1 14927 fsum1p 14929 fsumsplitsnun 14931 fsum2dlem 14946 fsumless 14972 fsumabs 14977 fsumrlim 14987 fsumo1 14988 o1fsum 14989 cvgcmpce 14994 fsumiun 14997 incexclem 15012 incexc 15013 isumltss 15024 climcndslem1 15025 climcndslem2 15026 mertenslem1 15061 bitsinv1 15612 bitsinvp1 15619 sylow2a 18462 fsumcn 23149 ovolfiniun 23773 volfiniun 23819 uniioombllem3 23857 itgfsum 24098 dvmptfsum 24243 vieta1lem2 24571 mtest 24663 birthdaylem2 25200 fsumharmonic 25259 ftalem5 25324 chtprm 25400 chtdif 25405 perfectlem2 25476 lgsquadlem2 25627 dchrisumlem1 25735 dchrisumlem2 25736 rpvmasum2 25758 dchrisum0lem1b 25761 dchrisum0lem3 25765 pntrsumbnd2 25813 pntrlog2bndlem6 25829 pntpbnd2 25833 pntlemf 25851 axlowdimlem16 26414 axlowdimlem17 26415 vtxdgoddnumeven 27006 indsumin 30854 signsplypnf 31393 fsum2dsub 31451 hgt750lemd 31492 tgoldbachgtde 31504 jm2.22 39028 jm2.23 39029 sumpair 40783 sumnnodd 41407 stoweidlem11 41792 stoweidlem26 41807 stoweidlem44 41825 sge0resplit 42184 sge0split 42187 fsumsplitsndif 43003 perfectALTVlem2 43323 |
Copyright terms: Public domain | W3C validator |