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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐾 ) ∈ ℂ )
2		faccl	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
4	3	nncnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
5		facne0	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ≠ 0 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ≠ 0 )
7	1 4 6	absdivd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝐾 ) ) / ( abs ‘ ( ! ‘ 𝐾 ) ) ) )
8		absexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝐾 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) )
9	3	nnred	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℝ )
10	3	nnnn0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℕ0 )
11	10	nn0ge0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ ( ! ‘ 𝐾 ) )
12	9 11	absidd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ! ‘ 𝐾 ) ) = ( ! ‘ 𝐾 ) )
13	8 12	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( 𝐴 ↑ 𝐾 ) ) / ( abs ‘ ( ! ‘ 𝐾 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) )
14	7 13	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) )