This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
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 } ) )