Theorem eftabs

Description: The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007)

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

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	adantl	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to K!\in \mathbb{N}$$
4	3	nncnd	$$⊢\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	absdivd	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \left|\frac{A^K}{K!}\right|=\frac{\left|A^K\right|}{\left|K!\right|}$$
8		absexp	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \left|A^K\right|={\left|A\right|}^K$$
9	3	nnred	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to K!\in ℝ$$
10	3	nnnn0d	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to K!\in {\mathbb{N}}_0$$
11	10	nn0ge0d	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to 0\le K!$$
12	9 11	absidd	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \left|K!\right|=K!$$
13	8 12	oveq12d	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \frac{\left|A^K\right|}{\left|K!\right|}=\frac{{\left|A\right|}^K}{K!}$$
14	7 13	eqtrd	$$⊢\left(A\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to \left|\frac{A^K}{K!}\right|=\frac{{\left|A\right|}^K}{K!}$$