Metamath Proof Explorer


Theorem esumadd

Description: Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Hypotheses esumadd.0 φ A V
esumadd.1 φ k A B 0 +∞
esumadd.2 φ k A C 0 +∞
Assertion esumadd φ * k A B + 𝑒 C = * k A B + 𝑒 * k A C

Proof

Step Hyp Ref Expression
1 esumadd.0 φ A V
2 esumadd.1 φ k A B 0 +∞
3 esumadd.2 φ k A C 0 +∞
4 nfv k φ
5 nfcv _ k A
6 ge0xaddcl B 0 +∞ C 0 +∞ B + 𝑒 C 0 +∞
7 2 3 6 syl2anc φ k A B + 𝑒 C 0 +∞
8 xrge0base 0 +∞ = Base 𝑠 * 𝑠 0 +∞
9 xrge0plusg + 𝑒 = + 𝑠 * 𝑠 0 +∞
10 xrge0cmn 𝑠 * 𝑠 0 +∞ CMnd
11 10 a1i φ 𝑠 * 𝑠 0 +∞ CMnd
12 xrge0tmd 𝑠 * 𝑠 0 +∞ TopMnd
13 12 a1i φ 𝑠 * 𝑠 0 +∞ TopMnd
14 2 fmpttd φ k A B : A 0 +∞
15 3 fmpttd φ k A C : A 0 +∞
16 4 5 1 2 esumel φ * k A B 𝑠 * 𝑠 0 +∞ tsums k A B
17 4 5 1 3 esumel φ * k A C 𝑠 * 𝑠 0 +∞ tsums k A C
18 8 9 11 13 1 14 15 16 17 tsmsadd φ * k A B + 𝑒 * k A C 𝑠 * 𝑠 0 +∞ tsums k A B + 𝑒 f k A C
19 eqidd φ k A B = k A B
20 eqidd φ k A C = k A C
21 1 2 3 19 20 offval2 φ k A B + 𝑒 f k A C = k A B + 𝑒 C
22 21 oveq2d φ 𝑠 * 𝑠 0 +∞ tsums k A B + 𝑒 f k A C = 𝑠 * 𝑠 0 +∞ tsums k A B + 𝑒 C
23 18 22 eleqtrd φ * k A B + 𝑒 * k A C 𝑠 * 𝑠 0 +∞ tsums k A B + 𝑒 C
24 4 5 1 7 23 esumid φ * k A B + 𝑒 C = * k A B + 𝑒 * k A C