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 = if k A C 0
sumsplit.6 φ k Z G k = if k B C 0
sumsplit.7 φ k A B C
sumsplit.8 φ seq M + F dom
sumsplit.9 φ seq M + G dom
Assertion sumsplit φ k A B C = k A C + k B C

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 = if k A C 0
6 sumsplit.6 φ k Z G k = if k B C 0
7 sumsplit.7 φ k A B C
8 sumsplit.8 φ seq M + F dom
9 sumsplit.9 φ seq M + G dom
10 7 ralrimiva φ k A B C
11 1 eqimssi Z M
12 11 a1i φ Z M
13 12 orcd φ Z M Z Fin
14 sumss2 A B Z k A B C Z M Z Fin k A B C = k Z if k A B C 0
15 4 10 13 14 syl21anc φ k A B C = k Z if k A B C 0
16 iftrue k A if k A C 0 = C
17 16 adantl φ k A if k A C 0 = C
18 elun1 k A k A B
19 18 7 sylan2 φ k A C
20 17 19 eqeltrd φ k A if k A C 0
21 iffalse ¬ k A if k A C 0 = 0
22 0cn 0
23 21 22 eqeltrdi ¬ k A if k A C 0
24 23 adantl φ ¬ k A if k A C 0
25 20 24 pm2.61dan φ if k A C 0
26 25 adantr φ k Z if k A C 0
27 iftrue k B if k B C 0 = C
28 27 adantl φ k B if k B C 0 = C
29 elun2 k B k A B
30 29 7 sylan2 φ k B C
31 28 30 eqeltrd φ k B if k B C 0
32 iffalse ¬ k B if k B C 0 = 0
33 32 22 eqeltrdi ¬ k B if k B C 0
34 33 adantl φ ¬ k B if k B C 0
35 31 34 pm2.61dan φ if k B C 0
36 35 adantr φ k Z if k B C 0
37 1 2 5 26 6 36 8 9 isumadd φ k Z if k A C 0 + if k B C 0 = k Z if k A C 0 + k Z if k B C 0
38 19 addid1d φ 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 if k B C 0 = 0
48 17 47 oveq12d φ k A if k A C 0 + if k B C 0 = C + 0
49 iftrue k A B if k A B C 0 = C
50 18 49 syl k A if k A B C 0 = C
51 50 adantl φ k A if k A B C 0 = C
52 38 48 51 3eqtr4rd φ k A if k A B C 0 = if k A C 0 + if k B C 0
53 35 addid2d φ 0 + if k B C 0 = if k B C 0
54 53 adantr φ ¬ k A 0 + if k B C 0 = if k B C 0
55 21 adantl φ ¬ k A if k A C 0 = 0
56 55 oveq1d φ ¬ k A if k A C 0 + if k B C 0 = 0 + if k B C 0
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 if k A B C 0 = if k B C 0
62 54 56 61 3eqtr4rd φ ¬ k A if k A B C 0 = if k A C 0 + if k B C 0
63 52 62 pm2.61dan φ if k A B C 0 = if k A C 0 + if k B C 0
64 63 sumeq2sdv φ k Z if k A B C 0 = k Z if k A C 0 + if k B C 0
65 4 unssad φ A Z
66 19 ralrimiva φ k A C
67 sumss2 A Z k A C Z M Z Fin k A C = k Z if k A C 0
68 65 66 13 67 syl21anc φ k A C = k Z if k A C 0
69 4 unssbd φ B Z
70 30 ralrimiva φ k B C
71 sumss2 B Z k B C Z M Z Fin k B C = k Z if k B C 0
72 69 70 13 71 syl21anc φ k B C = k Z if k B C 0
73 68 72 oveq12d φ k A C + k B C = k Z if k A C 0 + k Z if k B C 0
74 37 64 73 3eqtr4rd φ k A C + k B C = k Z if k A B C 0
75 15 74 eqtr4d φ k A B C = k A C + k B C