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

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 mullidi 
 |-  ( 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 mulridi 
 |-  ( ( 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 ) ) ) )