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	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
Assertion	eftlcl	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		eftl.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
3		nn0z	$$⊢M\in {\mathbb{N}}_0\to M\in \mathbb{Z}$$
4	3	adantl	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to M\in \mathbb{Z}$$
5		eqidd	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=F\left(k\right)$$
6		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{N}}_0$$
7	6	adantll	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{N}}_0$$
8	1	eftval	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{A^k}{k!}$$
9	7 8	syl	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=\frac{A^k}{k!}$$
10		simpll	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to A\in ℂ$$
11		eftcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \frac{A^k}{k!}\in ℂ$$
12	10 7 11	syl2anc	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \frac{A^k}{k!}\in ℂ$$
13	9 12	eqeltrd	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)\in ℂ$$
14	1	eftlcvg	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
15	2 4 5 13 14	isumcl	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)\in ℂ$$