Theorem ser0f

Description: A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ser0.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2	1	ser0	⊢ ( 𝑘 ∈ 𝑍 → ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑘 ) = 0 )
3		c0ex	⊢ 0 ∈ V
4	3	fvconst2	⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑍 × { 0 } ) ‘ 𝑘 ) = 0 )
5	2 4	eqtr4d	⊢ ( 𝑘 ∈ 𝑍 → ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 0 } ) ‘ 𝑘 ) )
6	5	rgen	⊢ ∀ 𝑘 ∈ 𝑍 ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 0 } ) ‘ 𝑘 )
7		seqfn	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
8	1	fneq2i	⊢ ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) Fn 𝑍 ↔ seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
9	7 8	sylibr	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) Fn 𝑍 )
10	3	fconst	⊢ ( 𝑍 × { 0 } ) : 𝑍 ⟶ { 0 }
11		ffn	⊢ ( ( 𝑍 × { 0 } ) : 𝑍 ⟶ { 0 } → ( 𝑍 × { 0 } ) Fn 𝑍 )
12	10 11	ax-mp	⊢ ( 𝑍 × { 0 } ) Fn 𝑍
13		eqfnfv	⊢ ( ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) Fn 𝑍 ∧ ( 𝑍 × { 0 } ) Fn 𝑍 ) → ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) = ( 𝑍 × { 0 } ) ↔ ∀ 𝑘 ∈ 𝑍 ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 0 } ) ‘ 𝑘 ) ) )
14	9 12 13	sylancl	⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) = ( 𝑍 × { 0 } ) ↔ ∀ 𝑘 ∈ 𝑍 ( seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 0 } ) ‘ 𝑘 ) ) )
15	6 14	mpbiri	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( 𝑍 × { 0 } ) ) = ( 𝑍 × { 0 } ) )