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 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion efi4p ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 efi4p.1 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 ax-icn i ∈ ℂ
3 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4 2 3 mpan ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
5 1 ef4p ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )
6 4 5 syl ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )
7 ax-1cn 1 ∈ ℂ
8 addcl ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
9 7 4 8 sylancr ( 𝐴 ∈ ℂ → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
10 4 sqcld ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) ∈ ℂ )
11 10 halfcld ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ∈ ℂ )
12 3nn0 3 ∈ ℕ0
13 expcl ( ( ( i · 𝐴 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ )
14 4 12 13 sylancl ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ )
15 6cn 6 ∈ ℂ
16 6re 6 ∈ ℝ
17 6pos 0 < 6
18 16 17 gt0ne0ii 6 ≠ 0
19 divcl ( ( ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ∈ ℂ )
20 15 18 19 mp3an23 ( ( ( i · 𝐴 ) ↑ 3 ) ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ∈ ℂ )
21 14 20 syl ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ∈ ℂ )
22 9 11 21 addassd ( 𝐴 ∈ ℂ → ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( ( 1 + ( i · 𝐴 ) ) + ( ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) )
23 7 a1i ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
24 23 4 11 21 add4d ( 𝐴 ∈ ℂ → ( ( 1 + ( i · 𝐴 ) ) + ( ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) = ( ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) )
25 2nn0 2 ∈ ℕ0
26 mulexp ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
27 2 25 26 mp3an13 ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
28 i2 ( i ↑ 2 ) = - 1
29 28 oveq1i ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
30 29 a1i ( 𝐴 ∈ ℂ → ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) ) )
31 sqcl ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
32 31 mulm1d ( 𝐴 ∈ ℂ → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
33 27 30 32 3eqtrd ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
34 33 oveq1d ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
35 2cn 2 ∈ ℂ
36 2ne0 2 ≠ 0
37 divneg ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( ( 𝐴 ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
38 35 36 37 mp3an23 ( ( 𝐴 ↑ 2 ) ∈ ℂ → - ( ( 𝐴 ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
39 31 38 syl ( 𝐴 ∈ ℂ → - ( ( 𝐴 ↑ 2 ) / 2 ) = ( - ( 𝐴 ↑ 2 ) / 2 ) )
40 34 39 eqtr4d ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) = - ( ( 𝐴 ↑ 2 ) / 2 ) )
41 40 oveq2d ( 𝐴 ∈ ℂ → ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) = ( 1 + - ( ( 𝐴 ↑ 2 ) / 2 ) ) )
42 31 halfcld ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℂ )
43 negsub ( ( 1 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℂ ) → ( 1 + - ( ( 𝐴 ↑ 2 ) / 2 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
44 7 42 43 sylancr ( 𝐴 ∈ ℂ → ( 1 + - ( ( 𝐴 ↑ 2 ) / 2 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
45 41 44 eqtrd ( 𝐴 ∈ ℂ → ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
46 mulexp ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( i · 𝐴 ) ↑ 3 ) = ( ( i ↑ 3 ) · ( 𝐴 ↑ 3 ) ) )
47 2 12 46 mp3an13 ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 3 ) = ( ( i ↑ 3 ) · ( 𝐴 ↑ 3 ) ) )
48 i3 ( i ↑ 3 ) = - i
49 48 oveq1i ( ( i ↑ 3 ) · ( 𝐴 ↑ 3 ) ) = ( - i · ( 𝐴 ↑ 3 ) )
50 47 49 eqtrdi ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 3 ) = ( - i · ( 𝐴 ↑ 3 ) ) )
51 50 oveq1d ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) = ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) )
52 expcl ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
53 12 52 mpan2 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 3 ) ∈ ℂ )
54 negicn - i ∈ ℂ
55 15 18 pm3.2i ( 6 ∈ ℂ ∧ 6 ≠ 0 )
56 divass ( ( - i ∈ ℂ ∧ ( 𝐴 ↑ 3 ) ∈ ℂ ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ) → ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) = ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) )
57 54 55 56 mp3an13 ( ( 𝐴 ↑ 3 ) ∈ ℂ → ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) = ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) )
58 53 57 syl ( 𝐴 ∈ ℂ → ( ( - i · ( 𝐴 ↑ 3 ) ) / 6 ) = ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) )
59 divcl ( ( ( 𝐴 ↑ 3 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
60 15 18 59 mp3an23 ( ( 𝐴 ↑ 3 ) ∈ ℂ → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
61 53 60 syl ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
62 mulneg12 ( ( i ∈ ℂ ∧ ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) )
63 2 61 62 sylancr ( 𝐴 ∈ ℂ → ( - i · ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) )
64 51 58 63 3eqtrd ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) = ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) )
65 64 oveq2d ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
66 61 negcld ( 𝐴 ∈ ℂ → - ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ )
67 adddi ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ - ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
68 2 67 mp3an1 ( ( 𝐴 ∈ ℂ ∧ - ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
69 66 68 mpdan ( 𝐴 ∈ ℂ → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( ( i · 𝐴 ) + ( i · - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
70 negsub ( ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℂ ) → ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) )
71 61 70 mpdan ( 𝐴 ∈ ℂ → ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) = ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) )
72 71 oveq2d ( 𝐴 ∈ ℂ → ( i · ( 𝐴 + - ( ( 𝐴 ↑ 3 ) / 6 ) ) ) = ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
73 65 69 72 3eqtr2d ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) )
74 45 73 oveq12d ( 𝐴 ∈ ℂ → ( ( 1 + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( i · 𝐴 ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) )
75 22 24 74 3eqtrd ( 𝐴 ∈ ℂ → ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) )
76 75 oveq1d ( 𝐴 ∈ ℂ → ( ( ( ( 1 + ( i · 𝐴 ) ) + ( ( ( i · 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( ( i · 𝐴 ) ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )
77 6 76 eqtrd ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )