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 e. RR /\ K e. NN0 ) -> ( ( A ^ K ) / ( ! ` K ) ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		reexpcl	|- ( ( A e. RR /\ K e. NN0 ) -> ( A ^ K ) e. RR )
2		faccl	|- ( K e. NN0 -> ( ! ` K ) e. NN )
3	2	adantl	|- ( ( A e. RR /\ K e. NN0 ) -> ( ! ` K ) e. NN )
4	1 3	nndivred	|- ( ( A e. RR /\ K e. NN0 ) -> ( ( A ^ K ) / ( ! ` K ) ) e. RR )