This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ( 𝐹 ‘ 𝑘 ) ) )