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 AeiA=cosAisinA

Proof

Step Hyp Ref Expression
1 ax-icn i
2 mulneg12 iAiA=iA
3 1 2 mpan AiA=iA
4 3 fveq2d AeiA=eiA
5 negcl AA
6 efival AeiA=cosA+isinA
7 5 6 syl AeiA=cosA+isinA
8 cosneg AcosA=cosA
9 sinneg AsinA=sinA
10 9 oveq2d AisinA=isinA
11 sincl AsinA
12 mulneg2 isinAisinA=isinA
13 1 11 12 sylancr AisinA=isinA
14 10 13 eqtrd AisinA=isinA
15 8 14 oveq12d AcosA+isinA=cosA+isinA
16 coscl AcosA
17 mulcl isinAisinA
18 1 11 17 sylancr AisinA
19 16 18 negsubd AcosA+isinA=cosAisinA
20 15 19 eqtrd AcosA+isinA=cosAisinA
21 7 20 eqtrd AeiA=cosAisinA
22 4 21 eqtrd AeiA=cosAisinA