Theorem serclim0

Description: The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008) (Proof shortened by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Assertion	serclim0	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ) ⇝ 0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
2	1	ser0f	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ) = ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) )
3		0cn	⊢ 0 ∈ ℂ
4		ssid	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝑀 )
5		fvex	⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
6	4 5	climconst2	⊢ ( ( 0 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ⇝ 0 )
7	3 6	mpan	⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ⇝ 0 )
8	2 7	eqbrtrd	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ) ⇝ 0 )