Theorem eftcl

Description: Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007)

	Ref	Expression
Assertion	eftcl	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \frac{A^K}{K!}\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		expcl	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to A^K\in ℂ$$
2		faccl	$$⊢K\in {\mathbb{N}}_0\to K!\in \mathbb{N}$$
3	2	nncnd	$$⊢K\in {\mathbb{N}}_0\to K!\in ℂ$$
4	3	adantl	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to K!\in ℂ$$
5		facne0	$$⊢K\in {\mathbb{N}}_0\to K!\ne 0$$
6	5	adantl	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to K!\ne 0$$
7	1 4 6	divcld	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \frac{A^K}{K!}\in ℂ$$