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	$$⊢\left(A\in ℝ\wedge K\in {\mathbb{N}}_0\right)\to \frac{A^K}{K!}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		reexpcl	$$⊢\left(A\in ℝ\wedge K\in {\mathbb{N}}_0\right)\to A^K\in ℝ$$
2		faccl	$$⊢K\in {\mathbb{N}}_0\to K!\in \mathbb{N}$$
3	2	adantl	$$⊢\left(A\in ℝ\wedge K\in {\mathbb{N}}_0\right)\to K!\in \mathbb{N}$$
4	1 3	nndivred	$$⊢\left(A\in ℝ\wedge K\in {\mathbb{N}}_0\right)\to \frac{A^K}{K!}\in ℝ$$