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 ‘ 𝐴 ) ) ) )