Theorem reeftcl

Description: The terms of the series expansion of the exponential function at a real number are real. (Contributed by Paul Chapman, 15-Jan-2008)

	Ref	Expression
Assertion	reeftcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐾 ) ∈ ℝ )
2		faccl	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
4	1 3	nndivred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ∈ ℝ )