Theorem eftlcl

Description: Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypothesis	eftl.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	eftlcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		eftl.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
3		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
5		eqidd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
6		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
7	6	adantll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
8	1	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
9	7 8	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
10		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℂ )
11		eftcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
12	10 7 11	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
13	9 12	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
14	1	eftlcvg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
15	2 4 5 13 14	isumcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )