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