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. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )

Proof

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