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