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 syl6eq 
 |-  ( 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 ) ) )