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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumadd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumadd.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
isumadd.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
isumadd.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
isumadd.7 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
isumadd.8 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
Assertion isumadd ( 𝜑 → Σ 𝑘 ∈ 𝑍 ( 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ 𝑍 𝐴 + Σ 𝑘 ∈ 𝑍 𝐵 ) )

Proof

Step Hyp Ref Expression
1 isumadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isumadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isumadd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4 isumadd.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5 isumadd.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
6 isumadd.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
7 isumadd.7 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
8 isumadd.8 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
9 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
10 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) )
11 9 10 oveq12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
12 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) )
13 ovex ⊢ ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) ∈ V
14 11 12 13 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
16 3 5 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 + 𝐵 ) )
17 15 16 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐴 + 𝐵 ) )
18 4 6 addcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
19 1 2 3 4 7 isumclim2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )
20 seqex ⊢ seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ V
21 20 a1i ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ V )
22 1 2 5 6 8 isumclim2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐵 )
23 3 4 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
24 1 2 23 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
25 24 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
26 5 6 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
27 1 2 26 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℂ )
28 27 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℂ )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
30 29 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
31 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝜑 )
32 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
33 32 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
34 33 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝑘 ∈ 𝑍 )
35 31 34 23 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
36 31 34 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
37 34 14 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
38 30 35 36 37 seradd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) )
39 1 2 19 21 22 25 28 38 climadd ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) + ( 𝐺 ‘ 𝑚 ) ) ) ) ⇝ ( Σ 𝑘 ∈ 𝑍 𝐴 + Σ 𝑘 ∈ 𝑍 𝐵 ) )
40 1 2 17 18 39 isumclim ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 ( 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ 𝑍 𝐴 + Σ 𝑘 ∈ 𝑍 𝐵 ) )