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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( i · 𝐵 ) ) ↔ ( ( cos ‘ 𝐴 ) = ( cos ‘ 𝐵 ) ∧ ( sin ‘ 𝐴 ) = ( sin ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
3		efival	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
4		efival	⊢ ( 𝐵 ∈ ℂ → ( exp ‘ ( i · 𝐵 ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) )
5	3 4	eqeqan12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( i · 𝐵 ) ) ↔ ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ) )
6	1 2 5	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( i · 𝐵 ) ) ↔ ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ) )
7		recoscl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
8		resincl	⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) ∈ ℝ )
9	7 8	jca	⊢ ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ∈ ℝ ) )
10		recoscl	⊢ ( 𝐵 ∈ ℝ → ( cos ‘ 𝐵 ) ∈ ℝ )
11		resincl	⊢ ( 𝐵 ∈ ℝ → ( sin ‘ 𝐵 ) ∈ ℝ )
12	10 11	jca	⊢ ( 𝐵 ∈ ℝ → ( ( cos ‘ 𝐵 ) ∈ ℝ ∧ ( sin ‘ 𝐵 ) ∈ ℝ ) )
13		cru	⊢ ( ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ∈ ℝ ) ∧ ( ( cos ‘ 𝐵 ) ∈ ℝ ∧ ( sin ‘ 𝐵 ) ∈ ℝ ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ↔ ( ( cos ‘ 𝐴 ) = ( cos ‘ 𝐵 ) ∧ ( sin ‘ 𝐴 ) = ( sin ‘ 𝐵 ) ) ) )
14	9 12 13	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ↔ ( ( cos ‘ 𝐴 ) = ( cos ‘ 𝐵 ) ∧ ( sin ‘ 𝐴 ) = ( sin ‘ 𝐵 ) ) ) )
15	6 14	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( i · 𝐵 ) ) ↔ ( ( cos ‘ 𝐴 ) = ( cos ‘ 𝐵 ) ∧ ( sin ‘ 𝐴 ) = ( sin ‘ 𝐵 ) ) ) )