This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \in ℝ \land K \in ℕ_{0}) \to \frac{A^{K}}{K!} \in ℝ$

Step	Hyp	Ref	Expression
1		reexpcl	$⊢ (A \in ℝ \land K \in ℕ_{0}) \to A^{K} \in ℝ$
2		faccl	$⊢ K \in ℕ_{0} \to K! \in ℕ$
3	2	adantl	$⊢ (A \in ℝ \land K \in ℕ_{0}) \to K! \in ℕ$
4	1 3	nndivred	$⊢ (A \in ℝ \land K \in ℕ_{0}) \to \frac{A^{K}}{K!} \in ℝ$