Theorem 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)

	Ref	Expression
Hypotheses	isumnn0nn.1	⊢ ( 𝑘 = 0 → 𝐴 = 𝐵 )
	isumnn0nn.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumnn0nn.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
	isumnn0nn.4	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	isumnn0nn	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐴 = ( 𝐵 + Σ 𝑘 ∈ ℕ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isumnn0nn.1	⊢ ( 𝑘 = 0 → 𝐴 = 𝐵 )
2		isumnn0nn.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
3		isumnn0nn.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
4		isumnn0nn.4	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
5		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
7	5 6 2 3 4	isum1p	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐴 = ( ( 𝐹 ‘ 0 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 ) )
8		fveq2	⊢ ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
9	8 1	eqeq12d	⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ 𝑘 ) = 𝐴 ↔ ( 𝐹 ‘ 0 ) = 𝐵 ) )
10	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) = 𝐴 )
11		0nn0	⊢ 0 ∈ ℕ0
12	11	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
13	9 10 12	rspcdva	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝐵 )
14		0p1e1	⊢ ( 0 + 1 ) = 1
15	14	fveq2i	⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
16		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
17	15 16	eqtr4i	⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
18	17	sumeq1i	⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 = Σ 𝑘 ∈ ℕ 𝐴
19	18	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )
20	13 19	oveq12d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ℕ 𝐴 ) )
21	7 20	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐴 = ( 𝐵 + Σ 𝑘 ∈ ℕ 𝐴 ) )