Metamath Proof Explorer

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 
|- Z = ( ZZ>= ` M )
Assertion ser0f 
|- ( M e. ZZ -> seq M ( + , ( Z X. { 0 } ) ) = ( Z X. { 0 } ) )

Proof

Step Hyp Ref Expression
1 ser0.1 
 |-  Z = ( ZZ>= ` M )
2 1 ser0 
 |-  ( k e. Z -> ( seq M ( + , ( Z X. { 0 } ) ) ` k ) = 0 )
3 c0ex 
 |-  0 e. _V
4 3 fvconst2 
 |-  ( k e. Z -> ( ( Z X. { 0 } ) ` k ) = 0 )
5 2 4 eqtr4d 
 |-  ( k e. Z -> ( seq M ( + , ( Z X. { 0 } ) ) ` k ) = ( ( Z X. { 0 } ) ` k ) )
6 5 rgen 
 |-  A. k e. Z ( seq M ( + , ( Z X. { 0 } ) ) ` k ) = ( ( Z X. { 0 } ) ` k )
7 seqfn 
 |-  ( M e. ZZ -> seq M ( + , ( Z X. { 0 } ) ) Fn ( ZZ>= ` M ) )
8 1 fneq2i 
 |-  ( seq M ( + , ( Z X. { 0 } ) ) Fn Z <-> seq M ( + , ( Z X. { 0 } ) ) Fn ( ZZ>= ` M ) )
9 7 8 sylibr 
 |-  ( M e. ZZ -> seq M ( + , ( Z X. { 0 } ) ) Fn Z )
10 3 fconst 
 |-  ( Z X. { 0 } ) : Z --> { 0 }
11 ffn 
 |-  ( ( Z X. { 0 } ) : Z --> { 0 } -> ( Z X. { 0 } ) Fn Z )
12 10 11 ax-mp 
 |-  ( Z X. { 0 } ) Fn Z
13 eqfnfv 
 |-  ( ( seq M ( + , ( Z X. { 0 } ) ) Fn Z /\ ( Z X. { 0 } ) Fn Z ) -> ( seq M ( + , ( Z X. { 0 } ) ) = ( Z X. { 0 } ) <-> A. k e. Z ( seq M ( + , ( Z X. { 0 } ) ) ` k ) = ( ( Z X. { 0 } ) ` k ) ) )
14 9 12 13 sylancl 
 |-  ( M e. ZZ -> ( seq M ( + , ( Z X. { 0 } ) ) = ( Z X. { 0 } ) <-> A. k e. Z ( seq M ( + , ( Z X. { 0 } ) ) ` k ) = ( ( Z X. { 0 } ) ` k ) ) )
15 6 14 mpbiri 
 |-  ( M e. ZZ -> seq M ( + , ( Z X. { 0 } ) ) = ( Z X. { 0 } ) )