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

Metamath Proof Explorer

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