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

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