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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}B}\leftrightarrow \left(\cos A=\cos B\wedge \sin A=\sin B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		recn	$$⊢B\in ℝ\to B\in ℂ$$
3		efival	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\cos A+\mathrm{i}\sin A$$
4		efival	$$⊢B\in ℂ\to {\mathrm{e}}^{\mathrm{i}B}=\cos B+\mathrm{i}\sin B$$
5	3 4	eqeqan12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left({\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}B}\leftrightarrow \cos A+\mathrm{i}\sin A=\cos B+\mathrm{i}\sin B\right)$$
6	1 2 5	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}B}\leftrightarrow \cos A+\mathrm{i}\sin A=\cos B+\mathrm{i}\sin B\right)$$
7		recoscl	$$⊢A\in ℝ\to \cos A\in ℝ$$
8		resincl	$$⊢A\in ℝ\to \sin A\in ℝ$$
9	7 8	jca	$$⊢A\in ℝ\to \left(\cos A\in ℝ\wedge \sin A\in ℝ\right)$$
10		recoscl	$$⊢B\in ℝ\to \cos B\in ℝ$$
11		resincl	$$⊢B\in ℝ\to \sin B\in ℝ$$
12	10 11	jca	$$⊢B\in ℝ\to \left(\cos B\in ℝ\wedge \sin B\in ℝ\right)$$
13		cru	$$⊢\left(\left(\cos A\in ℝ\wedge \sin A\in ℝ\right)\wedge \left(\cos B\in ℝ\wedge \sin B\in ℝ\right)\right)\to \left(\cos A+\mathrm{i}\sin A=\cos B+\mathrm{i}\sin B\leftrightarrow \left(\cos A=\cos B\wedge \sin A=\sin B\right)\right)$$
14	9 12 13	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\cos A+\mathrm{i}\sin A=\cos B+\mathrm{i}\sin B\leftrightarrow \left(\cos A=\cos B\wedge \sin A=\sin B\right)\right)$$
15	6 14	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}B}\leftrightarrow \left(\cos A=\cos B\wedge \sin A=\sin B\right)\right)$$