Metamath Proof Explorer


Theorem efival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion efival ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn i ∈ ℂ
2 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
3 1 2 mpan ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
4 efcl ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
5 3 4 syl ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
6 negicn - i ∈ ℂ
7 mulcl ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
8 6 7 mpan ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
9 efcl ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
10 8 9 syl ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
11 5 10 addcld ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
12 5 10 subcld ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
13 2cn 2 ∈ ℂ
14 2ne0 2 ≠ 0
15 13 14 pm3.2i ( 2 ∈ ℂ ∧ 2 ≠ 0 )
16 divdir ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) + ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) )
17 15 16 mp3an3 ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) + ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) )
18 11 12 17 syl2anc ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) + ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) )
19 10 5 pncan3d ( 𝐴 ∈ ℂ → ( ( exp ‘ ( - i · 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( exp ‘ ( i · 𝐴 ) ) )
20 19 oveq2d ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) + ( ( exp ‘ ( - i · 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( i · 𝐴 ) ) ) )
21 5 10 12 addassd ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) + ( ( exp ‘ ( - i · 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
22 5 2timesd ( 𝐴 ∈ ℂ → ( 2 · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( i · 𝐴 ) ) ) )
23 20 21 22 3eqtr4d ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( 2 · ( exp ‘ ( i · 𝐴 ) ) ) )
24 23 oveq1d ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / 2 ) = ( ( 2 · ( exp ‘ ( i · 𝐴 ) ) ) / 2 ) )
25 divcan3 ( ( ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( exp ‘ ( i · 𝐴 ) ) ) / 2 ) = ( exp ‘ ( i · 𝐴 ) ) )
26 13 14 25 mp3an23 ( ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ → ( ( 2 · ( exp ‘ ( i · 𝐴 ) ) ) / 2 ) = ( exp ‘ ( i · 𝐴 ) ) )
27 5 26 syl ( 𝐴 ∈ ℂ → ( ( 2 · ( exp ‘ ( i · 𝐴 ) ) ) / 2 ) = ( exp ‘ ( i · 𝐴 ) ) )
28 24 27 eqtr2d ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / 2 ) )
29 cosval ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
30 2mulicn ( 2 · i ) ∈ ℂ
31 2muline0 ( 2 · i ) ≠ 0
32 30 31 pm3.2i ( ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 )
33 div12 ( ( i ∈ ℂ ∧ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) ) → ( i · ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( i / ( 2 · i ) ) ) )
34 1 32 33 mp3an13 ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ → ( i · ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( i / ( 2 · i ) ) ) )
35 12 34 syl ( 𝐴 ∈ ℂ → ( i · ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( i / ( 2 · i ) ) ) )
36 sinval ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
37 36 oveq2d ( 𝐴 ∈ ℂ → ( i · ( sin ‘ 𝐴 ) ) = ( i · ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) ) )
38 divrec ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( 1 / 2 ) ) )
39 13 14 38 mp3an23 ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( 1 / 2 ) ) )
40 12 39 syl ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( 1 / 2 ) ) )
41 1 mulid2i ( 1 · i ) = i
42 41 oveq1i ( ( 1 · i ) / ( 2 · i ) ) = ( i / ( 2 · i ) )
43 ine0 i ≠ 0
44 1 43 dividi ( i / i ) = 1
45 44 oveq2i ( ( 1 / 2 ) · ( i / i ) ) = ( ( 1 / 2 ) · 1 )
46 ax-1cn 1 ∈ ℂ
47 46 13 1 1 14 43 divmuldivi ( ( 1 / 2 ) · ( i / i ) ) = ( ( 1 · i ) / ( 2 · i ) )
48 45 47 eqtr3i ( ( 1 / 2 ) · 1 ) = ( ( 1 · i ) / ( 2 · i ) )
49 halfcn ( 1 / 2 ) ∈ ℂ
50 49 mulid1i ( ( 1 / 2 ) · 1 ) = ( 1 / 2 )
51 48 50 eqtr3i ( ( 1 · i ) / ( 2 · i ) ) = ( 1 / 2 )
52 42 51 eqtr3i ( i / ( 2 · i ) ) = ( 1 / 2 )
53 52 oveq2i ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( i / ( 2 · i ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( 1 / 2 ) )
54 40 53 eqtr4di ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) · ( i / ( 2 · i ) ) ) )
55 35 37 54 3eqtr4d ( 𝐴 ∈ ℂ → ( i · ( sin ‘ 𝐴 ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
56 29 55 oveq12d ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) + ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) )
57 18 28 56 3eqtr4d ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )