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

Proof

Step	Hyp	Ref	Expression
1		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐾 ) ∈ ℂ )
2		faccl	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
3	2	nncnd	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℂ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
5		facne0	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ≠ 0 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ≠ 0 )
7	1 4 6	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ∈ ℂ )