fsumsplit - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fsumsplit		Structured version Visualization version GIF version

Theorem fsumsplit 15707

Description: Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)

**Hypotheses**
Ref	Expression
fsumsplit.1	⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
fsumsplit.2	⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))
fsumsplit.3	⊢ (𝜑 → 𝑈 ∈ Fin)
fsumsplit.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)

**Assertion**
Ref	Expression
fsumsplit	⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝜑,𝑘 𝑈,𝑘 Allowed substitution hint: 𝐶(𝑘)

**Proof of Theorem fsumsplit**
Step	Hyp	Ref	Expression
1		ssun1 4141	. . . . 5 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		fsumsplit.2	. . . . 5 ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))
3	1, 2	sseqtrrid 3990	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
4	3	sselda 3946	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑈)
5		fsumsplit.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)
6	4, 5	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
7	6	ralrimiva 3125	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
8		fsumsplit.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ Fin)
9	8	olcd 874	. . . 4 ⊢ (𝜑 → (𝑈 ⊆ (ℤ_≥‘0) ∨ 𝑈 ∈ Fin))
10		sumss2 15692	. . . 4 ⊢ (((𝐴 ⊆ 𝑈 ∧ ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) ∧ (𝑈 ⊆ (ℤ_≥‘0) ∨ 𝑈 ∈ Fin)) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0))
11	3, 7, 9, 10	syl21anc 837	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0))
12		ssun2 4142	. . . . 5 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
13	12, 2	sseqtrrid 3990	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ 𝑈)
14	13	sselda 3946	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝑈)
15	14, 5	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
16	15	ralrimiva 3125	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
17		sumss2 15692	. . . 4 ⊢ (((𝐵 ⊆ 𝑈 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) ∧ (𝑈 ⊆ (ℤ_≥‘0) ∨ 𝑈 ∈ Fin)) → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0))
18	13, 16, 9, 17	syl21anc 837	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0))
19	11, 18	oveq12d 7405	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0)))
20		0cn 11166	. . . 4 ⊢ 0 ∈ ℂ
21		ifcl 4534	. . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ)
22	5, 20, 21	sylancl 586	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ)
23		ifcl 4534	. . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ)
24	5, 20, 23	sylancl 586	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ)
25	8, 22, 24	fsumadd 15706	. 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0)))
26	2	eleq2d 2814	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵)))
27		elun 4116	. . . . . 6 ⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))
28	26, 27	bitrdi 287	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)))
29	28	biimpa 476	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))
30		iftrue 4494	. . . . . . . 8 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶)
31	30	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶)
32		noel 4301	. . . . . . . . . . 11 ⊢ ¬ 𝑘 ∈ ∅
33		fsumsplit.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
34	33	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ 𝑘 ∈ ∅))
35		elin 3930	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))
36	34, 35	bitr3di 286	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ ∅ ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)))
37	32, 36	mtbii 326	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))
38		imnan 399	. . . . . . . . . 10 ⊢ ((𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵) ↔ ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))
39	37, 38	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵))
40	39	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵)
41	40	iffalsed 4499	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 0)
42	31, 41	oveq12d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (𝐶 + 0))
43	6	addridd 11374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 + 0) = 𝐶)
44	42, 43	eqtrd 2764	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶)
45	39	con2d 134	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴))
46	45	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 ∈ 𝐴)
47	46	iffalsed 4499	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 0)
48		iftrue 4494	. . . . . . . 8 ⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶)
49	48	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶)
50	47, 49	oveq12d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (0 + 𝐶))
51	15	addlidd 11375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (0 + 𝐶) = 𝐶)
52	50, 51	eqtrd 2764	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶)
53	44, 52	jaodan 959	. . . 4 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶)
54	29, 53	syldan 591	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶)
55	54	sumeq2dv 15668	. 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = Σ𝑘 ∈ 𝑈 𝐶)
56	19, 25, 55	3eqtr2rd 2771	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 ifcif 4488 ‘cfv 6511 (class class class)co 7387 Fincfn 8918 ℂcc 11066 0cc0 11068 + caddc 11071 ℤ_≥cuz 12793 Σcsu 15652

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 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

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 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-z 12530 df-uz 12794 df-rp 12952 df-fz 13469 df-fzo 13616 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653

This theorem is referenced by: fsumsplitf 15708 sumpr 15714 sumtp 15715 fsumm1 15717 fsum1p 15719 fsumsplitsnun 15721 fsum2dlem 15736 fsumless 15762 fsumabs 15767 fsumrlim 15777 fsumo1 15778 o1fsum 15779 cvgcmpce 15784 fsumiun 15787 incexclem 15802 incexc 15803 isumltss 15814 climcndslem1 15815 climcndslem2 15816 mertenslem1 15850 bitsinv1 16412 bitsinvp1 16419 sylow2a 19549 fsumcn 24761 ovolfiniun 25402 volfiniun 25448 uniioombllem3 25486 itgfsum 25728 dvmptfsum 25879 vieta1lem2 26219 mtest 26313 birthdaylem2 26862 fsumharmonic 26922 ftalem5 26987 chtprm 27063 chtdif 27068 perfectlem2 27141 lgsquadlem2 27292 dchrisumlem1 27400 dchrisumlem2 27401 rpvmasum2 27423 dchrisum0lem1b 27426 dchrisum0lem3 27430 pntrsumbnd2 27478 pntrlog2bndlem6 27494 pntpbnd2 27498 pntlemf 27516 axlowdimlem16 28884 axlowdimlem17 28885 vtxdgoddnumeven 29481 indsumin 32785 signsplypnf 34541 fsum2dsub 34598 hgt750lemd 34639 tgoldbachgtde 34651 sticksstones6 42139 sticksstones7 42140 sumcubes 42301 jm2.22 42984 jm2.23 42985 sumpair 45029 sumnnodd 45628 stoweidlem11 46009 stoweidlem26 46024 stoweidlem44 46042 sge0resplit 46404 sge0split 46407 fsumsplitsndif 47374 perfectALTVlem2 47723

W3C validator