Metamath Proof Explorer

Theorem sumsplit

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

Ref Expression
Hypotheses sumsplit.1 ⊢Z=ℤ≥M
sumsplit.2 ⊢φ→M∈ℤ
sumsplit.3 ⊢φ→A∩B=∅
sumsplit.4 ⊢φ→A∪B⊆Z
sumsplit.5 ⊢φ∧k∈Z→F⁡k=ifk∈AC0
sumsplit.6 ⊢φ∧k∈Z→G⁡k=ifk∈BC0
sumsplit.7 ⊢φ∧k∈A∪B→C∈ℂ
sumsplit.8 ⊢φ→seqM+F∈dom⁡⇝
sumsplit.9 ⊢φ→seqM+G∈dom⁡⇝
Assertion sumsplit ⊢φ→∑k∈A∪BC=∑k∈AC+∑k∈BC

Proof

Step Hyp Ref Expression
1 sumsplit.1 ⊢Z=ℤ≥M
2 sumsplit.2 ⊢φ→M∈ℤ
3 sumsplit.3 ⊢φ→A∩B=∅
4 sumsplit.4 ⊢φ→A∪B⊆Z
5 sumsplit.5 ⊢φ∧k∈Z→F⁡k=ifk∈AC0
6 sumsplit.6 ⊢φ∧k∈Z→G⁡k=ifk∈BC0
7 sumsplit.7 ⊢φ∧k∈A∪B→C∈ℂ
8 sumsplit.8 ⊢φ→seqM+F∈dom⁡⇝
9 sumsplit.9 ⊢φ→seqM+G∈dom⁡⇝
10 7 ralrimiva ⊢φ→∀k∈A∪BC∈ℂ
11 1 eqimssi ⊢Z⊆ℤ≥M
12 11 a1i ⊢φ→Z⊆ℤ≥M
13 12 orcd ⊢φ→Z⊆ℤ≥M∨Z∈Fin
14 sumss2 ⊢A∪B⊆Z∧∀k∈A∪BC∈ℂ∧Z⊆ℤ≥M∨Z∈Fin→∑k∈A∪BC=∑k∈Zifk∈A∪BC0
15 4 10 13 14 syl21anc ⊢φ→∑k∈A∪BC=∑k∈Zifk∈A∪BC0
16 iftrue ⊢k∈A→ifk∈AC0=C
17 16 adantl ⊢φ∧k∈A→ifk∈AC0=C
18 elun1 ⊢k∈A→k∈A∪B
19 18 7 sylan2 ⊢φ∧k∈A→C∈ℂ
20 17 19 eqeltrd ⊢φ∧k∈A→ifk∈AC0∈ℂ
21 iffalse ⊢¬k∈A→ifk∈AC0=0
22 0cn ⊢0∈ℂ
23 21 22 eqeltrdi ⊢¬k∈A→ifk∈AC0∈ℂ
24 23 adantl ⊢φ∧¬k∈A→ifk∈AC0∈ℂ
25 20 24 pm2.61dan ⊢φ→ifk∈AC0∈ℂ
26 25 adantr ⊢φ∧k∈Z→ifk∈AC0∈ℂ
27 iftrue ⊢k∈B→ifk∈BC0=C
28 27 adantl ⊢φ∧k∈B→ifk∈BC0=C
29 elun2 ⊢k∈B→k∈A∪B
30 29 7 sylan2 ⊢φ∧k∈B→C∈ℂ
31 28 30 eqeltrd ⊢φ∧k∈B→ifk∈BC0∈ℂ
32 iffalse ⊢¬k∈B→ifk∈BC0=0
33 32 22 eqeltrdi ⊢¬k∈B→ifk∈BC0∈ℂ
34 33 adantl ⊢φ∧¬k∈B→ifk∈BC0∈ℂ
35 31 34 pm2.61dan ⊢φ→ifk∈BC0∈ℂ
36 35 adantr ⊢φ∧k∈Z→ifk∈BC0∈ℂ
37 1 2 5 26 6 36 8 9 isumadd ⊢φ→∑k∈Zifk∈AC0+ifk∈BC0=∑k∈Zifk∈AC0+∑k∈Zifk∈BC0
38 19 addridd ⊢φ∧k∈A→C+0=C
39 noel ⊢¬k∈∅
40 3 eleq2d ⊢φ→k∈A∩B↔k∈∅
41 elin ⊢k∈A∩B↔k∈A∧k∈B
42 40 41 bitr3di ⊢φ→k∈∅↔k∈A∧k∈B
43 39 42 mtbii ⊢φ→¬k∈A∧k∈B
44 imnan ⊢k∈A→¬k∈B↔¬k∈A∧k∈B
45 43 44 sylibr ⊢φ→k∈A→¬k∈B
46 45 imp ⊢φ∧k∈A→¬k∈B
47 46 32 syl ⊢φ∧k∈A→ifk∈BC0=0
48 17 47 oveq12d ⊢φ∧k∈A→ifk∈AC0+ifk∈BC0=C+0
49 iftrue ⊢k∈A∪B→ifk∈A∪BC0=C
50 18 49 syl ⊢k∈A→ifk∈A∪BC0=C
51 50 adantl ⊢φ∧k∈A→ifk∈A∪BC0=C
52 38 48 51 3eqtr4rd ⊢φ∧k∈A→ifk∈A∪BC0=ifk∈AC0+ifk∈BC0
53 35 addlidd ⊢φ→0+ifk∈BC0=ifk∈BC0
54 53 adantr ⊢φ∧¬k∈A→0+ifk∈BC0=ifk∈BC0
55 21 adantl ⊢φ∧¬k∈A→ifk∈AC0=0
56 55 oveq1d ⊢φ∧¬k∈A→ifk∈AC0+ifk∈BC0=0+ifk∈BC0
57 elun ⊢k∈A∪B↔k∈A∨k∈B
58 biorf ⊢¬k∈A→k∈B↔k∈A∨k∈B
59 57 58 bitr4id ⊢¬k∈A→k∈A∪B↔k∈B
60 59 adantl ⊢φ∧¬k∈A→k∈A∪B↔k∈B
61 60 ifbid ⊢φ∧¬k∈A→ifk∈A∪BC0=ifk∈BC0
62 54 56 61 3eqtr4rd ⊢φ∧¬k∈A→ifk∈A∪BC0=ifk∈AC0+ifk∈BC0
63 52 62 pm2.61dan ⊢φ→ifk∈A∪BC0=ifk∈AC0+ifk∈BC0
64 63 sumeq2sdv ⊢φ→∑k∈Zifk∈A∪BC0=∑k∈Zifk∈AC0+ifk∈BC0
65 4 unssad ⊢φ→A⊆Z
66 19 ralrimiva ⊢φ→∀k∈AC∈ℂ
67 sumss2 ⊢A⊆Z∧∀k∈AC∈ℂ∧Z⊆ℤ≥M∨Z∈Fin→∑k∈AC=∑k∈Zifk∈AC0
68 65 66 13 67 syl21anc ⊢φ→∑k∈AC=∑k∈Zifk∈AC0
69 4 unssbd ⊢φ→B⊆Z
70 30 ralrimiva ⊢φ→∀k∈BC∈ℂ
71 sumss2 ⊢B⊆Z∧∀k∈BC∈ℂ∧Z⊆ℤ≥M∨Z∈Fin→∑k∈BC=∑k∈Zifk∈BC0
72 69 70 13 71 syl21anc ⊢φ→∑k∈BC=∑k∈Zifk∈BC0
73 68 72 oveq12d ⊢φ→∑k∈AC+∑k∈BC=∑k∈Zifk∈AC0+∑k∈Zifk∈BC0
74 37 64 73 3eqtr4rd ⊢φ→∑k∈AC+∑k∈BC=∑k∈Zifk∈A∪BC0
75 15 74 eqtr4d ⊢φ→∑k∈A∪BC=∑k∈AC+∑k∈BC