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 ⊢ A ∈ ℂ → e A = e ℜ ⁡ A ⁢ cos ⁡ ℑ ⁡ A + i ⁢ sin ⁡ ℑ ⁡ A

Proof

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