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	syl6eqr	|- ( 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 ) ) ) )