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	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to \|\frac{A^{K}}{K!}\| = \frac{{\|A\|}^{K}}{K!}$

Step	Hyp	Ref	Expression
1		expcl	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to A^{K} \in ℂ$
2		faccl	$⊢ K \in ℕ_{0} \to K! \in ℕ$
3	2	adantl	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to K! \in ℕ$
4	3	nncnd	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to K! \in ℂ$
5		facne0	$⊢ K \in ℕ_{0} \to K! \neq 0$
6	5	adantl	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to K! \neq 0$
7	1 4 6	absdivd	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to \|\frac{A^{K}}{K!}\| = \frac{\|A^{K}\|}{\|K!\|}$
8		absexp	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to \|A^{K}\| = {\|A\|}^{K}$
9	3	nnred	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to K! \in ℝ$
10	3	nnnn0d	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to K! \in ℕ_{0}$
11	10	nn0ge0d	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to 0 \leq K!$
12	9 11	absidd	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to \|K!\| = K!$
13	8 12	oveq12d	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to \frac{\|A^{K}\|}{\|K!\|} = \frac{{\|A\|}^{K}}{K!}$
14	7 13	eqtrd	$⊢ (A \in ℂ \land K \in ℕ_{0}) \to \|\frac{A^{K}}{K!}\| = \frac{{\|A\|}^{K}}{K!}$

Metamath Proof Explorer