Metamath Proof Explorer

Theorem efmival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006)

Ref Expression
Assertion efmival ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 mulneg12 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
4 3 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) = ( exp ‘ ( i · - 𝐴 ) ) )
5 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
6 efival ⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) )
7 5 6 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) )
8 cosneg ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
9 sinneg ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = - ( sin ‘ 𝐴 ) )
10 9 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( sin ‘ - 𝐴 ) ) = ( i · - ( sin ‘ 𝐴 ) ) )
11 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
12 mulneg2 ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · - ( sin ‘ 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
13 1 11 12 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · - ( sin ‘ 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
14 10 13 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( i · ( sin ‘ - 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
15 8 14 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) )
16 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
17 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
18 1 11 17 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
19 16 18 negsubd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
20 15 19 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
21 7 20 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
22 4 21 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )