This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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