Metamath Proof Explorer

Theorem ef4p

Description: Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypothesis ef4p.1 
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion ef4p 
|- ( A e. CC -> ( exp ` A ) = ( ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / 6 ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )

Proof

Step Hyp Ref Expression
1 ef4p.1 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 df-4 
 |-  4 = ( 3 + 1 )
3 3nn0 
 |-  3 e. NN0
4 id 
 |-  ( A e. CC -> A e. CC )
5 ax-1cn 
 |-  1 e. CC
6 addcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 + A ) e. CC )
7 5 6 mpan 
 |-  ( A e. CC -> ( 1 + A ) e. CC )
8 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
9 8 halfcld 
 |-  ( A e. CC -> ( ( A ^ 2 ) / 2 ) e. CC )
10 7 9 addcld 
 |-  ( A e. CC -> ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) e. CC )
11 df-3 
 |-  3 = ( 2 + 1 )
12 2nn0 
 |-  2 e. NN0
13 df-2 
 |-  2 = ( 1 + 1 )
14 1nn0 
 |-  1 e. NN0
15 5 a1i 
 |-  ( A e. CC -> 1 e. CC )
16 1e0p1 
 |-  1 = ( 0 + 1 )
17 0nn0 
 |-  0 e. NN0
18 0cnd 
 |-  ( A e. CC -> 0 e. CC )
19 1 efval2 
 |-  ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( F ` k ) )
20 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
21 20 sumeq1i 
 |-  sum_ k e. NN0 ( F ` k ) = sum_ k e. ( ZZ>= ` 0 ) ( F ` k )
22 19 21 eqtr2di 
 |-  ( A e. CC -> sum_ k e. ( ZZ>= ` 0 ) ( F ` k ) = ( exp ` A ) )
23 22 oveq2d 
 |-  ( A e. CC -> ( 0 + sum_ k e. ( ZZ>= ` 0 ) ( F ` k ) ) = ( 0 + ( exp ` A ) ) )
24 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
25 24 addid2d 
 |-  ( A e. CC -> ( 0 + ( exp ` A ) ) = ( exp ` A ) )
26 23 25 eqtr2d 
 |-  ( A e. CC -> ( exp ` A ) = ( 0 + sum_ k e. ( ZZ>= ` 0 ) ( F ` k ) ) )
27 eft0val 
 |-  ( A e. CC -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = 1 )
28 27 oveq2d 
 |-  ( A e. CC -> ( 0 + ( ( A ^ 0 ) / ( ! ` 0 ) ) ) = ( 0 + 1 ) )
29 0p1e1 
 |-  ( 0 + 1 ) = 1
30 28 29 eqtrdi 
 |-  ( A e. CC -> ( 0 + ( ( A ^ 0 ) / ( ! ` 0 ) ) ) = 1 )
31 1 16 17 4 18 26 30 efsep 
 |-  ( A e. CC -> ( exp ` A ) = ( 1 + sum_ k e. ( ZZ>= ` 1 ) ( F ` k ) ) )
32 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
33 fac1 
 |-  ( ! ` 1 ) = 1
34 33 a1i 
 |-  ( A e. CC -> ( ! ` 1 ) = 1 )
35 32 34 oveq12d 
 |-  ( A e. CC -> ( ( A ^ 1 ) / ( ! ` 1 ) ) = ( A / 1 ) )
36 div1 
 |-  ( A e. CC -> ( A / 1 ) = A )
37 35 36 eqtrd 
 |-  ( A e. CC -> ( ( A ^ 1 ) / ( ! ` 1 ) ) = A )
38 37 oveq2d 
 |-  ( A e. CC -> ( 1 + ( ( A ^ 1 ) / ( ! ` 1 ) ) ) = ( 1 + A ) )
39 1 13 14 4 15 31 38 efsep 
 |-  ( A e. CC -> ( exp ` A ) = ( ( 1 + A ) + sum_ k e. ( ZZ>= ` 2 ) ( F ` k ) ) )
40 fac2 
 |-  ( ! ` 2 ) = 2
41 40 oveq2i 
 |-  ( ( A ^ 2 ) / ( ! ` 2 ) ) = ( ( A ^ 2 ) / 2 )
42 41 oveq2i 
 |-  ( ( 1 + A ) + ( ( A ^ 2 ) / ( ! ` 2 ) ) ) = ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) )
43 42 a1i 
 |-  ( A e. CC -> ( ( 1 + A ) + ( ( A ^ 2 ) / ( ! ` 2 ) ) ) = ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) )
44 1 11 12 4 7 39 43 efsep 
 |-  ( A e. CC -> ( exp ` A ) = ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + sum_ k e. ( ZZ>= ` 3 ) ( F ` k ) ) )
45 fac3 
 |-  ( ! ` 3 ) = 6
46 45 oveq2i 
 |-  ( ( A ^ 3 ) / ( ! ` 3 ) ) = ( ( A ^ 3 ) / 6 )
47 46 oveq2i 
 |-  ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / ( ! ` 3 ) ) ) = ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / 6 ) )
48 47 a1i 
 |-  ( A e. CC -> ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / ( ! ` 3 ) ) ) = ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / 6 ) ) )
49 1 2 3 4 10 44 48 efsep 
 |-  ( A e. CC -> ( exp ` A ) = ( ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / 6 ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )