Theorem efieq

Description: The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008)

	Ref	Expression
Assertion	efieq	|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` ( _i x. A ) ) = ( exp ` ( _i x. B ) ) <-> ( ( cos ` A ) = ( cos ` B ) /\ ( sin ` A ) = ( sin ` B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2		recn	|- ( B e. RR -> B e. CC )
3		efival	|- ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
4		efival	|- ( B e. CC -> ( exp ` ( _i x. B ) ) = ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) )
5	3 4	eqeqan12d	|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( _i x. A ) ) = ( exp ` ( _i x. B ) ) <-> ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) = ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) ) )
6	1 2 5	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` ( _i x. A ) ) = ( exp ` ( _i x. B ) ) <-> ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) = ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) ) )
7		recoscl	|- ( A e. RR -> ( cos ` A ) e. RR )
8		resincl	|- ( A e. RR -> ( sin ` A ) e. RR )
9	7 8	jca	|- ( A e. RR -> ( ( cos ` A ) e. RR /\ ( sin ` A ) e. RR ) )
10		recoscl	|- ( B e. RR -> ( cos ` B ) e. RR )
11		resincl	|- ( B e. RR -> ( sin ` B ) e. RR )
12	10 11	jca	|- ( B e. RR -> ( ( cos ` B ) e. RR /\ ( sin ` B ) e. RR ) )
13		cru	|- ( ( ( ( cos ` A ) e. RR /\ ( sin ` A ) e. RR ) /\ ( ( cos ` B ) e. RR /\ ( sin ` B ) e. RR ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) = ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) <-> ( ( cos ` A ) = ( cos ` B ) /\ ( sin ` A ) = ( sin ` B ) ) ) )
14	9 12 13	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) = ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) <-> ( ( cos ` A ) = ( cos ` B ) /\ ( sin ` A ) = ( sin ` B ) ) ) )
15	6 14	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` ( _i x. A ) ) = ( exp ` ( _i x. B ) ) <-> ( ( cos ` A ) = ( cos ` B ) /\ ( sin ` A ) = ( sin ` B ) ) ) )