Theorem efeul

Description: Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006)

	Ref	Expression
Assertion	efeul	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( ( cos ‘ ( ℑ ‘ 𝐴 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝐴 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		replim	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
2	1	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( exp ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
3		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
4	3	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
5		ax-icn	⊢ i ∈ ℂ
6		imcl	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
7	6	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
8		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
9	5 7 8	sylancr	⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
10		efadd	⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
11	4 9 10	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
12		efival	⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℂ → ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝐴 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝐴 ) ) ) ) )
13	7 12	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝐴 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝐴 ) ) ) ) )
14	13	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( ( cos ‘ ( ℑ ‘ 𝐴 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝐴 ) ) ) ) ) )
15	2 11 14	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( ( cos ‘ ( ℑ ‘ 𝐴 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝐴 ) ) ) ) ) )