# 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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 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 ‘ 𝐵 ) ) ) )