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

Metamath Proof Explorer

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 )