Metamath Proof Explorer


Theorem efi4p

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, 30-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 efi4p.1
 |-  F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
2 ax-icn
 |-  _i e. CC
3 mulcl
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4 2 3 mpan
 |-  ( A e. CC -> ( _i x. A ) e. CC )
5 1 ef4p
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) = ( ( ( ( 1 + ( _i x. A ) ) + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
6 4 5 syl
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( ( ( 1 + ( _i x. A ) ) + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
7 ax-1cn
 |-  1 e. CC
8 addcl
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
9 7 4 8 sylancr
 |-  ( A e. CC -> ( 1 + ( _i x. A ) ) e. CC )
10 4 sqcld
 |-  ( A e. CC -> ( ( _i x. A ) ^ 2 ) e. CC )
11 10 halfcld
 |-  ( A e. CC -> ( ( ( _i x. A ) ^ 2 ) / 2 ) e. CC )
12 3nn0
 |-  3 e. NN0
13 expcl
 |-  ( ( ( _i x. A ) e. CC /\ 3 e. NN0 ) -> ( ( _i x. A ) ^ 3 ) e. CC )
14 4 12 13 sylancl
 |-  ( A e. CC -> ( ( _i x. A ) ^ 3 ) e. CC )
15 6cn
 |-  6 e. CC
16 6re
 |-  6 e. RR
17 6pos
 |-  0 < 6
18 16 17 gt0ne0ii
 |-  6 =/= 0
19 divcl
 |-  ( ( ( ( _i x. A ) ^ 3 ) e. CC /\ 6 e. CC /\ 6 =/= 0 ) -> ( ( ( _i x. A ) ^ 3 ) / 6 ) e. CC )
20 15 18 19 mp3an23
 |-  ( ( ( _i x. A ) ^ 3 ) e. CC -> ( ( ( _i x. A ) ^ 3 ) / 6 ) e. CC )
21 14 20 syl
 |-  ( A e. CC -> ( ( ( _i x. A ) ^ 3 ) / 6 ) e. CC )
22 9 11 21 addassd
 |-  ( A e. CC -> ( ( ( 1 + ( _i x. A ) ) + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) = ( ( 1 + ( _i x. A ) ) + ( ( ( ( _i x. A ) ^ 2 ) / 2 ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) ) )
23 7 a1i
 |-  ( A e. CC -> 1 e. CC )
24 23 4 11 21 add4d
 |-  ( A e. CC -> ( ( 1 + ( _i x. A ) ) + ( ( ( ( _i x. A ) ^ 2 ) / 2 ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) ) = ( ( 1 + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( _i x. A ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) ) )
25 2nn0
 |-  2 e. NN0
26 mulexp
 |-  ( ( _i e. CC /\ A e. CC /\ 2 e. NN0 ) -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) )
27 2 25 26 mp3an13
 |-  ( A e. CC -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) )
28 i2
 |-  ( _i ^ 2 ) = -u 1
29 28 oveq1i
 |-  ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = ( -u 1 x. ( A ^ 2 ) )
30 29 a1i
 |-  ( A e. CC -> ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = ( -u 1 x. ( A ^ 2 ) ) )
31 sqcl
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
32 31 mulm1d
 |-  ( A e. CC -> ( -u 1 x. ( A ^ 2 ) ) = -u ( A ^ 2 ) )
33 27 30 32 3eqtrd
 |-  ( A e. CC -> ( ( _i x. A ) ^ 2 ) = -u ( A ^ 2 ) )
34 33 oveq1d
 |-  ( A e. CC -> ( ( ( _i x. A ) ^ 2 ) / 2 ) = ( -u ( A ^ 2 ) / 2 ) )
35 2cn
 |-  2 e. CC
36 2ne0
 |-  2 =/= 0
37 divneg
 |-  ( ( ( A ^ 2 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( ( A ^ 2 ) / 2 ) = ( -u ( A ^ 2 ) / 2 ) )
38 35 36 37 mp3an23
 |-  ( ( A ^ 2 ) e. CC -> -u ( ( A ^ 2 ) / 2 ) = ( -u ( A ^ 2 ) / 2 ) )
39 31 38 syl
 |-  ( A e. CC -> -u ( ( A ^ 2 ) / 2 ) = ( -u ( A ^ 2 ) / 2 ) )
40 34 39 eqtr4d
 |-  ( A e. CC -> ( ( ( _i x. A ) ^ 2 ) / 2 ) = -u ( ( A ^ 2 ) / 2 ) )
41 40 oveq2d
 |-  ( A e. CC -> ( 1 + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) = ( 1 + -u ( ( A ^ 2 ) / 2 ) ) )
42 31 halfcld
 |-  ( A e. CC -> ( ( A ^ 2 ) / 2 ) e. CC )
43 negsub
 |-  ( ( 1 e. CC /\ ( ( A ^ 2 ) / 2 ) e. CC ) -> ( 1 + -u ( ( A ^ 2 ) / 2 ) ) = ( 1 - ( ( A ^ 2 ) / 2 ) ) )
44 7 42 43 sylancr
 |-  ( A e. CC -> ( 1 + -u ( ( A ^ 2 ) / 2 ) ) = ( 1 - ( ( A ^ 2 ) / 2 ) ) )
45 41 44 eqtrd
 |-  ( A e. CC -> ( 1 + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) = ( 1 - ( ( A ^ 2 ) / 2 ) ) )
46 mulexp
 |-  ( ( _i e. CC /\ A e. CC /\ 3 e. NN0 ) -> ( ( _i x. A ) ^ 3 ) = ( ( _i ^ 3 ) x. ( A ^ 3 ) ) )
47 2 12 46 mp3an13
 |-  ( A e. CC -> ( ( _i x. A ) ^ 3 ) = ( ( _i ^ 3 ) x. ( A ^ 3 ) ) )
48 i3
 |-  ( _i ^ 3 ) = -u _i
49 48 oveq1i
 |-  ( ( _i ^ 3 ) x. ( A ^ 3 ) ) = ( -u _i x. ( A ^ 3 ) )
50 47 49 eqtrdi
 |-  ( A e. CC -> ( ( _i x. A ) ^ 3 ) = ( -u _i x. ( A ^ 3 ) ) )
51 50 oveq1d
 |-  ( A e. CC -> ( ( ( _i x. A ) ^ 3 ) / 6 ) = ( ( -u _i x. ( A ^ 3 ) ) / 6 ) )
52 expcl
 |-  ( ( A e. CC /\ 3 e. NN0 ) -> ( A ^ 3 ) e. CC )
53 12 52 mpan2
 |-  ( A e. CC -> ( A ^ 3 ) e. CC )
54 negicn
 |-  -u _i e. CC
55 15 18 pm3.2i
 |-  ( 6 e. CC /\ 6 =/= 0 )
56 divass
 |-  ( ( -u _i e. CC /\ ( A ^ 3 ) e. CC /\ ( 6 e. CC /\ 6 =/= 0 ) ) -> ( ( -u _i x. ( A ^ 3 ) ) / 6 ) = ( -u _i x. ( ( A ^ 3 ) / 6 ) ) )
57 54 55 56 mp3an13
 |-  ( ( A ^ 3 ) e. CC -> ( ( -u _i x. ( A ^ 3 ) ) / 6 ) = ( -u _i x. ( ( A ^ 3 ) / 6 ) ) )
58 53 57 syl
 |-  ( A e. CC -> ( ( -u _i x. ( A ^ 3 ) ) / 6 ) = ( -u _i x. ( ( A ^ 3 ) / 6 ) ) )
59 divcl
 |-  ( ( ( A ^ 3 ) e. CC /\ 6 e. CC /\ 6 =/= 0 ) -> ( ( A ^ 3 ) / 6 ) e. CC )
60 15 18 59 mp3an23
 |-  ( ( A ^ 3 ) e. CC -> ( ( A ^ 3 ) / 6 ) e. CC )
61 53 60 syl
 |-  ( A e. CC -> ( ( A ^ 3 ) / 6 ) e. CC )
62 mulneg12
 |-  ( ( _i e. CC /\ ( ( A ^ 3 ) / 6 ) e. CC ) -> ( -u _i x. ( ( A ^ 3 ) / 6 ) ) = ( _i x. -u ( ( A ^ 3 ) / 6 ) ) )
63 2 61 62 sylancr
 |-  ( A e. CC -> ( -u _i x. ( ( A ^ 3 ) / 6 ) ) = ( _i x. -u ( ( A ^ 3 ) / 6 ) ) )
64 51 58 63 3eqtrd
 |-  ( A e. CC -> ( ( ( _i x. A ) ^ 3 ) / 6 ) = ( _i x. -u ( ( A ^ 3 ) / 6 ) ) )
65 64 oveq2d
 |-  ( A e. CC -> ( ( _i x. A ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) = ( ( _i x. A ) + ( _i x. -u ( ( A ^ 3 ) / 6 ) ) ) )
66 61 negcld
 |-  ( A e. CC -> -u ( ( A ^ 3 ) / 6 ) e. CC )
67 adddi
 |-  ( ( _i e. CC /\ A e. CC /\ -u ( ( A ^ 3 ) / 6 ) e. CC ) -> ( _i x. ( A + -u ( ( A ^ 3 ) / 6 ) ) ) = ( ( _i x. A ) + ( _i x. -u ( ( A ^ 3 ) / 6 ) ) ) )
68 2 67 mp3an1
 |-  ( ( A e. CC /\ -u ( ( A ^ 3 ) / 6 ) e. CC ) -> ( _i x. ( A + -u ( ( A ^ 3 ) / 6 ) ) ) = ( ( _i x. A ) + ( _i x. -u ( ( A ^ 3 ) / 6 ) ) ) )
69 66 68 mpdan
 |-  ( A e. CC -> ( _i x. ( A + -u ( ( A ^ 3 ) / 6 ) ) ) = ( ( _i x. A ) + ( _i x. -u ( ( A ^ 3 ) / 6 ) ) ) )
70 negsub
 |-  ( ( A e. CC /\ ( ( A ^ 3 ) / 6 ) e. CC ) -> ( A + -u ( ( A ^ 3 ) / 6 ) ) = ( A - ( ( A ^ 3 ) / 6 ) ) )
71 61 70 mpdan
 |-  ( A e. CC -> ( A + -u ( ( A ^ 3 ) / 6 ) ) = ( A - ( ( A ^ 3 ) / 6 ) ) )
72 71 oveq2d
 |-  ( A e. CC -> ( _i x. ( A + -u ( ( A ^ 3 ) / 6 ) ) ) = ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) )
73 65 69 72 3eqtr2d
 |-  ( A e. CC -> ( ( _i x. A ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) = ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) )
74 45 73 oveq12d
 |-  ( A e. CC -> ( ( 1 + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( _i x. A ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) )
75 22 24 74 3eqtrd
 |-  ( A e. CC -> ( ( ( 1 + ( _i x. A ) ) + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) )
76 75 oveq1d
 |-  ( A e. CC -> ( ( ( ( 1 + ( _i x. A ) ) + ( ( ( _i x. A ) ^ 2 ) / 2 ) ) + ( ( ( _i x. A ) ^ 3 ) / 6 ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) = ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
77 6 76 eqtrd
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )