Metamath Proof Explorer

Theorem efcvgfsum

Description: Exponential function convergence in terms of a sequence of partial finite sums. (Contributed by NM, 10-Jan-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis efcvgfsum.1 
|- F = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ^ k ) / ( ! ` k ) ) )
Assertion efcvgfsum 
|- ( A e. CC -> F ~~> ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 efcvgfsum.1 
 |-  F = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ^ k ) / ( ! ` k ) ) )
2 oveq2 
 |-  ( n = j -> ( 0 ... n ) = ( 0 ... j ) )
3 2 sumeq1d 
 |-  ( n = j -> sum_ k e. ( 0 ... n ) ( ( A ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... j ) ( ( A ^ k ) / ( ! ` k ) ) )
4 sumex 
 |-  sum_ k e. ( 0 ... j ) ( ( A ^ k ) / ( ! ` k ) ) e. _V
5 3 1 4 fvmpt 
 |-  ( j e. NN0 -> ( F ` j ) = sum_ k e. ( 0 ... j ) ( ( A ^ k ) / ( ! ` k ) ) )
6 5 adantl 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( F ` j ) = sum_ k e. ( 0 ... j ) ( ( A ^ k ) / ( ! ` k ) ) )
7 elfznn0 
 |-  ( k e. ( 0 ... j ) -> k e. NN0 )
8 7 adantl 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> k e. NN0 )
9 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
10 9 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
11 8 10 syl 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
12 simpr 
 |-  ( ( A e. CC /\ j e. NN0 ) -> j e. NN0 )
13 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
14 12 13 eleqtrdi 
 |-  ( ( A e. CC /\ j e. NN0 ) -> j e. ( ZZ>= ` 0 ) )
15 simpll 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> A e. CC )
16 eftcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
17 15 8 16 syl2anc 
 |-  ( ( ( A e. CC /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
18 11 14 17 fsumser 
 |-  ( ( A e. CC /\ j e. NN0 ) -> sum_ k e. ( 0 ... j ) ( ( A ^ k ) / ( ! ` k ) ) = ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) )
19 6 18 eqtrd 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( F ` j ) = ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) )
20 19 ralrimiva 
 |-  ( A e. CC -> A. j e. NN0 ( F ` j ) = ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) )
21 sumex 
 |-  sum_ k e. ( 0 ... n ) ( ( A ^ k ) / ( ! ` k ) ) e. _V
22 21 1 fnmpti 
 |-  F Fn NN0
23 0z 
 |-  0 e. ZZ
24 seqfn 
 |-  ( 0 e. ZZ -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) Fn ( ZZ>= ` 0 ) )
25 23 24 ax-mp 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) Fn ( ZZ>= ` 0 )
26 13 fneq2i 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) Fn NN0 <-> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) Fn ( ZZ>= ` 0 ) )
27 25 26 mpbir 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) Fn NN0
28 eqfnfv 
 |-  ( ( F Fn NN0 /\ seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) Fn NN0 ) -> ( F = seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) <-> A. j e. NN0 ( F ` j ) = ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) ) )
29 22 27 28 mp2an 
 |-  ( F = seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) <-> A. j e. NN0 ( F ` j ) = ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` j ) )
30 20 29 sylibr 
 |-  ( A e. CC -> F = seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) )
31 9 efcvg 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` A ) )
32 30 31 eqbrtrd 
 |-  ( A e. CC -> F ~~> ( exp ` A ) )