Metamath Proof Explorer


Theorem sumss

Description: Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014)

Ref Expression
Hypotheses sumss.1 ( 𝜑𝐴𝐵 )
sumss.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
sumss.3 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
sumss.4 ( 𝜑𝐵 ⊆ ( ℤ𝑀 ) )
Assertion sumss ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 sumss.1 ( 𝜑𝐴𝐵 )
2 sumss.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
3 sumss.3 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
4 sumss.4 ( 𝜑𝐵 ⊆ ( ℤ𝑀 ) )
5 eqid ( ℤ𝑀 ) = ( ℤ𝑀 )
6 simpr ( ( 𝜑𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
7 1 4 sstrd ( 𝜑𝐴 ⊆ ( ℤ𝑀 ) )
8 7 adantr ( ( 𝜑𝑀 ∈ ℤ ) → 𝐴 ⊆ ( ℤ𝑀 ) )
9 nfcv 𝑘 𝑚
10 nffvmpt1 𝑘 ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 )
11 nfv 𝑘 𝑚𝐴
12 nffvmpt1 𝑘 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 )
13 nfcv 𝑘 0
14 11 12 13 nfif 𝑘 if ( 𝑚𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) , 0 )
15 10 14 nfeq 𝑘 ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) , 0 )
16 fveq2 ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) )
17 eleq1w ( 𝑘 = 𝑚 → ( 𝑘𝐴𝑚𝐴 ) )
18 fveq2 ( 𝑘 = 𝑚 → ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) = ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) )
19 17 18 ifbieq1d ( 𝑘 = 𝑚 → if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) = if ( 𝑚𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) , 0 ) )
20 16 19 eqeq12d ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) ↔ ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) , 0 ) ) )
21 eqid ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) = ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) )
22 21 fvmpt2i ( 𝑘 ∈ ( ℤ𝑀 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( I ‘ if ( 𝑘𝐴 , 𝐶 , 0 ) ) )
23 iftrue ( 𝑘𝐴 → if ( 𝑘𝐴 , 𝐶 , 0 ) = 𝐶 )
24 23 fveq2d ( 𝑘𝐴 → ( I ‘ if ( 𝑘𝐴 , 𝐶 , 0 ) ) = ( I ‘ 𝐶 ) )
25 22 24 sylan9eq ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
26 iftrue ( 𝑘𝐴 → if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) = ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) )
27 eqid ( 𝑘𝐴𝐶 ) = ( 𝑘𝐴𝐶 )
28 27 fvmpt2i ( 𝑘𝐴 → ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
29 26 28 eqtrd ( 𝑘𝐴 → if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
30 29 adantl ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ 𝑘𝐴 ) → if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
31 25 30 eqtr4d ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) )
32 iffalse ( ¬ 𝑘𝐴 → if ( 𝑘𝐴 , 𝐶 , 0 ) = 0 )
33 32 fveq2d ( ¬ 𝑘𝐴 → ( I ‘ if ( 𝑘𝐴 , 𝐶 , 0 ) ) = ( I ‘ 0 ) )
34 0z 0 ∈ ℤ
35 fvi ( 0 ∈ ℤ → ( I ‘ 0 ) = 0 )
36 34 35 ax-mp ( I ‘ 0 ) = 0
37 33 36 eqtrdi ( ¬ 𝑘𝐴 → ( I ‘ if ( 𝑘𝐴 , 𝐶 , 0 ) ) = 0 )
38 22 37 sylan9eq ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ ¬ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = 0 )
39 iffalse ( ¬ 𝑘𝐴 → if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
40 39 adantl ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ ¬ 𝑘𝐴 ) → if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
41 38 40 eqtr4d ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ ¬ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) )
42 31 41 pm2.61dan ( 𝑘 ∈ ( ℤ𝑀 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑘 ) , 0 ) )
43 9 15 20 42 vtoclgaf ( 𝑚 ∈ ( ℤ𝑀 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) , 0 ) )
44 43 adantl ( ( ( 𝜑𝑀 ∈ ℤ ) ∧ 𝑚 ∈ ( ℤ𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐴 , ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) , 0 ) )
45 2 fmpttd ( 𝜑 → ( 𝑘𝐴𝐶 ) : 𝐴 ⟶ ℂ )
46 45 adantr ( ( 𝜑𝑀 ∈ ℤ ) → ( 𝑘𝐴𝐶 ) : 𝐴 ⟶ ℂ )
47 46 ffvelrnda ( ( ( 𝜑𝑀 ∈ ℤ ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) ∈ ℂ )
48 5 6 8 44 47 zsum ( ( 𝜑𝑀 ∈ ℤ ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ) ) )
49 4 adantr ( ( 𝜑𝑀 ∈ ℤ ) → 𝐵 ⊆ ( ℤ𝑀 ) )
50 nfv 𝑘 𝜑
51 nfv 𝑘 𝑚𝐵
52 nffvmpt1 𝑘 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 )
53 51 52 13 nfif 𝑘 if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 )
54 10 53 nfeq 𝑘 ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 )
55 50 54 nfim 𝑘 ( 𝜑 → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) )
56 eleq1w ( 𝑘 = 𝑚 → ( 𝑘𝐵𝑚𝐵 ) )
57 fveq2 ( 𝑘 = 𝑚 → ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
58 56 57 ifbieq1d ( 𝑘 = 𝑚 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) )
59 16 58 eqeq12d ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) ↔ ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) ) )
60 59 imbi2d ( 𝑘 = 𝑚 → ( ( 𝜑 → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) ) ↔ ( 𝜑 → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) ) ) )
61 25 adantll ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
62 1 adantr ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → 𝐴𝐵 )
63 62 sselda ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → 𝑘𝐵 )
64 iftrue ( 𝑘𝐵 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) )
65 eqid ( 𝑘𝐵𝐶 ) = ( 𝑘𝐵𝐶 )
66 65 fvmpt2i ( 𝑘𝐵 → ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
67 64 66 eqtrd ( 𝑘𝐵 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
68 63 67 syl ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
69 61 68 eqtr4d ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) )
70 38 adantll ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ ¬ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = 0 )
71 67 ad2antrl ( ( 𝜑 ∧ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) ) → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
72 eldif ( 𝑘 ∈ ( 𝐵𝐴 ) ↔ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) )
73 3 fveq2d ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → ( I ‘ 𝐶 ) = ( I ‘ 0 ) )
74 0cn 0 ∈ ℂ
75 fvi ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
76 74 75 ax-mp ( I ‘ 0 ) = 0
77 73 76 eqtrdi ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → ( I ‘ 𝐶 ) = 0 )
78 72 77 sylan2br ( ( 𝜑 ∧ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) ) → ( I ‘ 𝐶 ) = 0 )
79 71 78 eqtrd ( ( 𝜑 ∧ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) ) → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
80 79 expr ( ( 𝜑𝑘𝐵 ) → ( ¬ 𝑘𝐴 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
81 iffalse ( ¬ 𝑘𝐵 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
82 81 adantl ( ( 𝜑 ∧ ¬ 𝑘𝐵 ) → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
83 82 a1d ( ( 𝜑 ∧ ¬ 𝑘𝐵 ) → ( ¬ 𝑘𝐴 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
84 80 83 pm2.61dan ( 𝜑 → ( ¬ 𝑘𝐴 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
85 84 adantr ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( ¬ 𝑘𝐴 → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
86 85 imp ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ ¬ 𝑘𝐴 ) → if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
87 70 86 eqtr4d ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ ¬ 𝑘𝐴 ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) )
88 69 87 pm2.61dan ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) )
89 88 expcom ( 𝑘 ∈ ( ℤ𝑀 ) → ( 𝜑 → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑘 ) , 0 ) ) )
90 9 55 60 89 vtoclgaf ( 𝑚 ∈ ( ℤ𝑀 ) → ( 𝜑 → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) ) )
91 90 impcom ( ( 𝜑𝑚 ∈ ( ℤ𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) )
92 91 adantlr ( ( ( 𝜑𝑀 ∈ ℤ ) ∧ 𝑚 ∈ ( ℤ𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚𝐵 , ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) , 0 ) )
93 2 ex ( 𝜑 → ( 𝑘𝐴𝐶 ∈ ℂ ) )
94 93 adantr ( ( 𝜑𝑘𝐵 ) → ( 𝑘𝐴𝐶 ∈ ℂ ) )
95 3 74 eqeltrdi ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 ∈ ℂ )
96 72 95 sylan2br ( ( 𝜑 ∧ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) ) → 𝐶 ∈ ℂ )
97 96 expr ( ( 𝜑𝑘𝐵 ) → ( ¬ 𝑘𝐴𝐶 ∈ ℂ ) )
98 94 97 pm2.61d ( ( 𝜑𝑘𝐵 ) → 𝐶 ∈ ℂ )
99 98 fmpttd ( 𝜑 → ( 𝑘𝐵𝐶 ) : 𝐵 ⟶ ℂ )
100 99 adantr ( ( 𝜑𝑀 ∈ ℤ ) → ( 𝑘𝐵𝐶 ) : 𝐵 ⟶ ℂ )
101 100 ffvelrnda ( ( ( 𝜑𝑀 ∈ ℤ ) ∧ 𝑚𝐵 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) ∈ ℂ )
102 5 6 49 92 101 zsum ( ( 𝜑𝑀 ∈ ℤ ) → Σ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ ( ℤ𝑀 ) ↦ if ( 𝑘𝐴 , 𝐶 , 0 ) ) ) ) )
103 48 102 eqtr4d ( ( 𝜑𝑀 ∈ ℤ ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = Σ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
104 sumfc Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = Σ 𝑘𝐴 𝐶
105 sumfc Σ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = Σ 𝑘𝐵 𝐶
106 103 104 105 3eqtr3g ( ( 𝜑𝑀 ∈ ℤ ) → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )
107 1 adantr ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴𝐵 )
108 uzf : ℤ ⟶ 𝒫 ℤ
109 108 fdmi dom ℤ = ℤ
110 109 eleq2i ( 𝑀 ∈ dom ℤ𝑀 ∈ ℤ )
111 ndmfv ( ¬ 𝑀 ∈ dom ℤ → ( ℤ𝑀 ) = ∅ )
112 110 111 sylnbir ( ¬ 𝑀 ∈ ℤ → ( ℤ𝑀 ) = ∅ )
113 112 sseq2d ( ¬ 𝑀 ∈ ℤ → ( 𝐵 ⊆ ( ℤ𝑀 ) ↔ 𝐵 ⊆ ∅ ) )
114 4 113 syl5ib ( ¬ 𝑀 ∈ ℤ → ( 𝜑𝐵 ⊆ ∅ ) )
115 114 impcom ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐵 ⊆ ∅ )
116 107 115 sstrd ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 ⊆ ∅ )
117 ss0 ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
118 116 117 syl ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 = ∅ )
119 ss0 ( 𝐵 ⊆ ∅ → 𝐵 = ∅ )
120 115 119 syl ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐵 = ∅ )
121 118 120 eqtr4d ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 = 𝐵 )
122 121 sumeq1d ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )
123 106 122 pm2.61dan ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )