Metamath Proof Explorer


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 ) → Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) ∈ ℂ )