isumnn0nn

Description: Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Step	Hyp	Ref	Expression
1		isumnn0nn.1	$⊢ k = 0 \to A = B$
2		isumnn0nn.2	$⊢ (φ \land k \in ℕ_{0}) \to F (k) = A$
3		isumnn0nn.3	$⊢ (φ \land k \in ℕ_{0}) \to A \in ℂ$
4		isumnn0nn.4	$⊢ φ \to seq 0 (+ F) \in dom ⇝$
5		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
6		0zd	$⊢ φ \to 0 \in ℤ$
7	5 6 2 3 4	isum1p	$⊢ φ \to \sum_{k \in ℕ_{0}} A = F (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} A$
8		fveq2	$⊢ k = 0 \to F (k) = F (0)$
9	8 1	eqeq12d	$⊢ k = 0 \to (F (k) = A \leftrightarrow F (0) = B)$
10	2	ralrimiva	$⊢ φ \to \forall k \in ℕ_{0} F (k) = A$
11		0nn0	$⊢ 0 \in ℕ_{0}$
12	11	a1i	$⊢ φ \to 0 \in ℕ_{0}$
13	9 10 12	rspcdva	$⊢ φ \to F (0) = B$
14		0p1e1	$⊢ 0 + 1 = 1$
15	14	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17	15 16	eqtr4i	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
18	17	sumeq1i	$⊢ \sum_{k \in ℤ_{\geq (0 + 1)}} A = \sum_{k \in ℕ} A$
19	18	a1i	$⊢ φ \to \sum_{k \in ℤ_{\geq (0 + 1)}} A = \sum_{k \in ℕ} A$
20	13 19	oveq12d	$⊢ φ \to F (0) + \sum_{k \in ℤ_{\geq (0 + 1)}} A = B + \sum_{k \in ℕ} A$
21	7 20	eqtrd	$⊢ φ \to \sum_{k \in ℕ_{0}} A = B + \sum_{k \in ℕ} A$

Metamath Proof Explorer