Theorem isum

Description: Series sum with an upper integer index set (i.e. an infinite series). (Contributed by Mario Carneiro, 15-Jul-2013) (Revised by Mario Carneiro, 7-Apr-2014)

	Ref	Expression
Hypotheses	zsum.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	zsum.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isum.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
	isum.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
Assertion	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zsum.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		zsum.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isum.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
4		isum.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
5		ssidd	⊢ ( 𝜑 → 𝑍 ⊆ 𝑍 )
6		iftrue	⊢ ( 𝑘 ∈ 𝑍 → if ( 𝑘 ∈ 𝑍 , 𝐵 , 0 ) = 𝐵 )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → if ( 𝑘 ∈ 𝑍 , 𝐵 , 0 ) = 𝐵 )
8	3 7	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝑍 , 𝐵 , 0 ) )
9	1 2 5 8 4	zsum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )