Theorem eftlcvg

Description: The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypothesis	eftl.1	|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion	eftlcvg	|- ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )

Proof

Step	Hyp	Ref	Expression
1		eftl.1	|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2	1	efcllem	|- ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )
3	2	adantr	|- ( ( A e. CC /\ M e. NN0 ) -> seq 0 ( + , F ) e. dom ~~> )
4		nn0uz	|- NN0 = ( ZZ>= ` 0 )
5		simpr	|- ( ( A e. CC /\ M e. NN0 ) -> M e. NN0 )
6	1	eftval	|- ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
7	6	adantl	|- ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
8		eftcl	|- ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
9	8	adantlr	|- ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
10	7 9	eqeltrd	|- ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( F ` k ) e. CC )
11	4 5 10	iserex	|- ( ( A e. CC /\ M e. NN0 ) -> ( seq 0 ( + , F ) e. dom ~~> <-> seq M ( + , F ) e. dom ~~> ) )
12	3 11	mpbid	|- ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )