Theorem ser0

Description: The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013) (Revised by Mario Carneiro, 15-Dec-2014)

	Ref	Expression
Hypothesis	ser0.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	ser0	⊢ ( 𝑁 ∈ 𝑍 → ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑁 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ser0.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		00id	⊢ ( 0 + 0 ) = 0
3	2	a1i	⊢ ( 𝑁 ∈ 𝑍 → ( 0 + 0 ) = 0 )
4	1	eleq2i	⊢ ( 𝑁 ∈ 𝑍 ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5	4	biimpi	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
6		0cn	⊢ 0 ∈ ℂ
7		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
8	7 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ 𝑍 )
9	8	adantl	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ 𝑍 )
10		fvconst2g	⊢ ( ( 0 ∈ ℂ ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 0 } ) ‘ 𝑘 ) = 0 )
11	6 9 10	sylancr	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑍 × { 0 } ) ‘ 𝑘 ) = 0 )
12	3 5 11	seqid3	⊢ ( 𝑁 ∈ 𝑍 → ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑁 ) = 0 )