Metamath Proof Explorer


Theorem isumadd

Description: Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumadd.1 Z = M
isumadd.2 φ M
isumadd.3 φ k Z F k = A
isumadd.4 φ k Z A
isumadd.5 φ k Z G k = B
isumadd.6 φ k Z B
isumadd.7 φ seq M + F dom
isumadd.8 φ seq M + G dom
Assertion isumadd φ k Z A + B = k Z A + k Z B

Proof

Step Hyp Ref Expression
1 isumadd.1 Z = M
2 isumadd.2 φ M
3 isumadd.3 φ k Z F k = A
4 isumadd.4 φ k Z A
5 isumadd.5 φ k Z G k = B
6 isumadd.6 φ k Z B
7 isumadd.7 φ seq M + F dom
8 isumadd.8 φ seq M + G dom
9 fveq2 m = k F m = F k
10 fveq2 m = k G m = G k
11 9 10 oveq12d m = k F m + G m = F k + G k
12 eqid m Z F m + G m = m Z F m + G m
13 ovex F k + G k V
14 11 12 13 fvmpt k Z m Z F m + G m k = F k + G k
15 14 adantl φ k Z m Z F m + G m k = F k + G k
16 3 5 oveq12d φ k Z F k + G k = A + B
17 15 16 eqtrd φ k Z m Z F m + G m k = A + B
18 4 6 addcld φ k Z A + B
19 1 2 3 4 7 isumclim2 φ seq M + F k Z A
20 seqex seq M + m Z F m + G m V
21 20 a1i φ seq M + m Z F m + G m V
22 1 2 5 6 8 isumclim2 φ seq M + G k Z B
23 3 4 eqeltrd φ k Z F k
24 1 2 23 serf φ seq M + F : Z
25 24 ffvelrnda φ j Z seq M + F j
26 5 6 eqeltrd φ k Z G k
27 1 2 26 serf φ seq M + G : Z
28 27 ffvelrnda φ j Z seq M + G j
29 simpr φ j Z j Z
30 29 1 eleqtrdi φ j Z j M
31 simpll φ j Z k M j φ
32 elfzuz k M j k M
33 32 1 eleqtrrdi k M j k Z
34 33 adantl φ j Z k M j k Z
35 31 34 23 syl2anc φ j Z k M j F k
36 31 34 26 syl2anc φ j Z k M j G k
37 34 14 syl φ j Z k M j m Z F m + G m k = F k + G k
38 30 35 36 37 seradd φ j Z seq M + m Z F m + G m j = seq M + F j + seq M + G j
39 1 2 19 21 22 25 28 38 climadd φ seq M + m Z F m + G m k Z A + k Z B
40 1 2 17 18 39 isumclim φ k Z A + B = k Z A + k Z B