# Metamath Proof Explorer

## 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 {ℕ}_{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 {ℕ}_{0}\right)\to {{A}}^{{K}}\in ℂ$
2 faccl ${⊢}{K}\in {ℕ}_{0}\to {K}!\in ℕ$
3 2 adantl ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to {K}!\in ℕ$
4 3 nncnd ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to {K}!\in ℂ$
5 facne0 ${⊢}{K}\in {ℕ}_{0}\to {K}!\ne 0$
6 5 adantl ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to {K}!\ne 0$
7 1 4 6 absdivd ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{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 {ℕ}_{0}\right)\to \left|{{A}}^{{K}}\right|={\left|{A}\right|}^{{K}}$
9 3 nnred ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to {K}!\in ℝ$
10 3 nnnn0d ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to {K}!\in {ℕ}_{0}$
11 10 nn0ge0d ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to 0\le {K}!$
12 9 11 absidd ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{0}\right)\to \left|{K}!\right|={K}!$
13 8 12 oveq12d ${⊢}\left({A}\in ℂ\wedge {K}\in {ℕ}_{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 {ℕ}_{0}\right)\to \left|\frac{{{A}}^{{K}}}{{K}!}\right|=\frac{{\left|{A}\right|}^{{K}}}{{K}!}$