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 ∈ ℝ ∧ B ∈ ℝ → e i ⁢ A = e i ⁢ B ↔ cos ⁡ A = cos ⁡ B ∧ sin ⁡ A = sin ⁡ B

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 recn ⊢ B ∈ ℝ → B ∈ ℂ
3 efival ⊢ A ∈ ℂ → e i ⁢ A = cos ⁡ A + i ⁢ sin ⁡ A
4 efival ⊢ B ∈ ℂ → e i ⁢ B = cos ⁡ B + i ⁢ sin ⁡ B
5 3 4 eqeqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → e i ⁢ A = e i ⁢ B ↔ cos ⁡ A + i ⁢ sin ⁡ A = cos ⁡ B + i ⁢ sin ⁡ B
6 1 2 5 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → e i ⁢ A = e i ⁢ B ↔ cos ⁡ A + i ⁢ sin ⁡ A = cos ⁡ B + i ⁢ sin ⁡ B
7 recoscl ⊢ A ∈ ℝ → cos ⁡ A ∈ ℝ
8 resincl ⊢ A ∈ ℝ → sin ⁡ A ∈ ℝ
9 7 8 jca ⊢ A ∈ ℝ → cos ⁡ A ∈ ℝ ∧ sin ⁡ A ∈ ℝ
10 recoscl ⊢ B ∈ ℝ → cos ⁡ B ∈ ℝ
11 resincl ⊢ B ∈ ℝ → sin ⁡ B ∈ ℝ
12 10 11 jca ⊢ B ∈ ℝ → cos ⁡ B ∈ ℝ ∧ sin ⁡ B ∈ ℝ
13 cru ⊢ cos ⁡ A ∈ ℝ ∧ sin ⁡ A ∈ ℝ ∧ cos ⁡ B ∈ ℝ ∧ sin ⁡ B ∈ ℝ → cos ⁡ A + i ⁢ sin ⁡ A = cos ⁡ B + i ⁢ sin ⁡ B ↔ cos ⁡ A = cos ⁡ B ∧ sin ⁡ A = sin ⁡ B
14 9 12 13 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → cos ⁡ A + i ⁢ sin ⁡ A = cos ⁡ B + i ⁢ sin ⁡ B ↔ cos ⁡ A = cos ⁡ B ∧ sin ⁡ A = sin ⁡ B
15 6 14 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → e i ⁢ A = e i ⁢ B ↔ cos ⁡ A = cos ⁡ B ∧ sin ⁡ A = sin ⁡ B