Theorem efmival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006)

	Ref	Expression
Assertion	efmival	|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2		mulneg12	|- ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = ( _i x. -u A ) )
3	1 2	mpan	|- ( A e. CC -> ( -u _i x. A ) = ( _i x. -u A ) )
4	3	fveq2d	|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( exp ` ( _i x. -u A ) ) )
5		negcl	|- ( A e. CC -> -u A e. CC )
6		efival	|- ( -u A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) )
7	5 6	syl	|- ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) )
8		cosneg	|- ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
9		sinneg	|- ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
10	9	oveq2d	|- ( A e. CC -> ( _i x. ( sin ` -u A ) ) = ( _i x. -u ( sin ` A ) ) )
11		sincl	|- ( A e. CC -> ( sin ` A ) e. CC )
12		mulneg2	|- ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
13	1 11 12	sylancr	|- ( A e. CC -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
14	10 13	eqtrd	|- ( A e. CC -> ( _i x. ( sin ` -u A ) ) = -u ( _i x. ( sin ` A ) ) )
15	8 14	oveq12d	|- ( A e. CC -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) )
16		coscl	|- ( A e. CC -> ( cos ` A ) e. CC )
17		mulcl	|- ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC )
18	1 11 17	sylancr	|- ( A e. CC -> ( _i x. ( sin ` A ) ) e. CC )
19	16 18	negsubd	|- ( A e. CC -> ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
20	15 19	eqtrd	|- ( A e. CC -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
21	7 20	eqtrd	|- ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
22	4 21	eqtrd	|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )