Metamath Proof Explorer

Theorem efsep

Description: Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses efsep.1 
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
efsep.2 
|- N = ( M + 1 )
efsep.3 
|- M e. NN0
efsep.4 
|- ( ph -> A e. CC )
efsep.5 
|- ( ph -> B e. CC )
efsep.6 
|- ( ph -> ( exp ` A ) = ( B + sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) )
efsep.7 
|- ( ph -> ( B + ( ( A ^ M ) / ( ! ` M ) ) ) = D )
Assertion efsep 
|- ( ph -> ( exp ` A ) = ( D + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) )

Proof

Step Hyp Ref Expression
1 efsep.1 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 efsep.2 
 |-  N = ( M + 1 )
3 efsep.3 
 |-  M e. NN0
4 efsep.4 
 |-  ( ph -> A e. CC )
5 efsep.5 
 |-  ( ph -> B e. CC )
6 efsep.6 
 |-  ( ph -> ( exp ` A ) = ( B + sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) )
7 efsep.7 
 |-  ( ph -> ( B + ( ( A ^ M ) / ( ! ` M ) ) ) = D )
8 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
9 3 nn0zi 
 |-  M e. ZZ
10 9 a1i 
 |-  ( ph -> M e. ZZ )
11 eqidd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( F ` k ) )
12 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
13 3 12 mpan 
 |-  ( k e. ( ZZ>= ` M ) -> k e. NN0 )
14 1 eftval 
 |-  ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
15 14 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
16 eftcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
17 4 16 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
18 15 17 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
19 13 18 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )
20 1 eftlcvg 
 |-  ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )
21 4 3 20 sylancl 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
22 8 10 11 19 21 isum1p 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) = ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) ( F ` k ) ) )
23 1 eftval 
 |-  ( M e. NN0 -> ( F ` M ) = ( ( A ^ M ) / ( ! ` M ) ) )
24 3 23 ax-mp 
 |-  ( F ` M ) = ( ( A ^ M ) / ( ! ` M ) )
25 2 eqcomi 
 |-  ( M + 1 ) = N
26 25 fveq2i 
 |-  ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` N )
27 26 sumeq1i 
 |-  sum_ k e. ( ZZ>= ` ( M + 1 ) ) ( F ` k ) = sum_ k e. ( ZZ>= ` N ) ( F ` k )
28 24 27 oveq12i 
 |-  ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) ( F ` k ) ) = ( ( ( A ^ M ) / ( ! ` M ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) )
29 22 28 eqtrdi 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) = ( ( ( A ^ M ) / ( ! ` M ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) )
30 29 oveq2d 
 |-  ( ph -> ( B + sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) = ( B + ( ( ( A ^ M ) / ( ! ` M ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) ) )
31 eftcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( ( A ^ M ) / ( ! ` M ) ) e. CC )
32 4 3 31 sylancl 
 |-  ( ph -> ( ( A ^ M ) / ( ! ` M ) ) e. CC )
33 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
34 3 33 ax-mp 
 |-  ( M + 1 ) e. NN0
35 2 34 eqeltri 
 |-  N e. NN0
36 1 eftlcl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> sum_ k e. ( ZZ>= ` N ) ( F ` k ) e. CC )
37 4 35 36 sylancl 
 |-  ( ph -> sum_ k e. ( ZZ>= ` N ) ( F ` k ) e. CC )
38 5 32 37 addassd 
 |-  ( ph -> ( ( B + ( ( A ^ M ) / ( ! ` M ) ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) = ( B + ( ( ( A ^ M ) / ( ! ` M ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) ) )
39 30 38 eqtr4d 
 |-  ( ph -> ( B + sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) = ( ( B + ( ( A ^ M ) / ( ! ` M ) ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) )
40 7 oveq1d 
 |-  ( ph -> ( ( B + ( ( A ^ M ) / ( ! ` M ) ) ) + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) = ( D + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) )
41 6 39 40 3eqtrd 
 |-  ( ph -> ( exp ` A ) = ( D + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) )