Metamath Proof Explorer


Theorem efival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion efival A e i A = cos A + i sin A

Proof

Step Hyp Ref Expression
1 ax-icn i
2 mulcl i A i A
3 1 2 mpan A i A
4 efcl i A e i A
5 3 4 syl A e i A
6 negicn i
7 mulcl i A i A
8 6 7 mpan A i A
9 efcl i A e i A
10 8 9 syl A e i A
11 5 10 addcld A e i A + e i A
12 5 10 subcld A e i A e i A
13 2cn 2
14 2ne0 2 0
15 13 14 pm3.2i 2 2 0
16 divdir e i A + e i A e i A e i A 2 2 0 e i A + e i A + e i A e i A 2 = e i A + e i A 2 + e i A e i A 2
17 15 16 mp3an3 e i A + e i A e i A e i A e i A + e i A + e i A e i A 2 = e i A + e i A 2 + e i A e i A 2
18 11 12 17 syl2anc A e i A + e i A + e i A e i A 2 = e i A + e i A 2 + e i A e i A 2
19 10 5 pncan3d A e i A + e i A - e i A = e i A
20 19 oveq2d A e i A + e i A + e i A e i A = e i A + e i A
21 5 10 12 addassd A e i A + e i A + e i A e i A = e i A + e i A + e i A e i A
22 5 2timesd A 2 e i A = e i A + e i A
23 20 21 22 3eqtr4d A e i A + e i A + e i A e i A = 2 e i A
24 23 oveq1d A e i A + e i A + e i A e i A 2 = 2 e i A 2
25 divcan3 e i A 2 2 0 2 e i A 2 = e i A
26 13 14 25 mp3an23 e i A 2 e i A 2 = e i A
27 5 26 syl A 2 e i A 2 = e i A
28 24 27 eqtr2d A e i A = e i A + e i A + e i A e i A 2
29 cosval A cos A = e i A + e i A 2
30 2mulicn 2 i
31 2muline0 2 i 0
32 30 31 pm3.2i 2 i 2 i 0
33 div12 i e i A e i A 2 i 2 i 0 i e i A e i A 2 i = e i A e i A i 2 i
34 1 32 33 mp3an13 e i A e i A i e i A e i A 2 i = e i A e i A i 2 i
35 12 34 syl A i e i A e i A 2 i = e i A e i A i 2 i
36 sinval A sin A = e i A e i A 2 i
37 36 oveq2d A i sin A = i e i A e i A 2 i
38 divrec e i A e i A 2 2 0 e i A e i A 2 = e i A e i A 1 2
39 13 14 38 mp3an23 e i A e i A e i A e i A 2 = e i A e i A 1 2
40 12 39 syl A e i A e i A 2 = e i A e i A 1 2
41 1 mulid2i 1 i = i
42 41 oveq1i 1 i 2 i = i 2 i
43 ine0 i 0
44 1 43 dividi i i = 1
45 44 oveq2i 1 2 i i = 1 2 1
46 ax-1cn 1
47 46 13 1 1 14 43 divmuldivi 1 2 i i = 1 i 2 i
48 45 47 eqtr3i 1 2 1 = 1 i 2 i
49 halfcn 1 2
50 49 mulid1i 1 2 1 = 1 2
51 48 50 eqtr3i 1 i 2 i = 1 2
52 42 51 eqtr3i i 2 i = 1 2
53 52 oveq2i e i A e i A i 2 i = e i A e i A 1 2
54 40 53 eqtr4di A e i A e i A 2 = e i A e i A i 2 i
55 35 37 54 3eqtr4d A i sin A = e i A e i A 2
56 29 55 oveq12d A cos A + i sin A = e i A + e i A 2 + e i A e i A 2
57 18 28 56 3eqtr4d A e i A = cos A + i sin A