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

Proof

Step	Hyp	Ref	Expression
1		expcl	|- ( ( A e. CC /\ K e. NN0 ) -> ( A ^ K ) e. CC )
2		faccl	|- ( K e. NN0 -> ( ! ` K ) e. NN )
3	2	nncnd	|- ( K e. NN0 -> ( ! ` K ) e. CC )
4	3	adantl	|- ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) e. CC )
5		facne0	|- ( K e. NN0 -> ( ! ` K ) =/= 0 )
6	5	adantl	|- ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) =/= 0 )
7	1 4 6	divcld	|- ( ( A e. CC /\ K e. NN0 ) -> ( ( A ^ K ) / ( ! ` K ) ) e. CC )