Metamath Proof Explorer

Theorem efieq1re

Description: A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008)

Ref Expression
Assertion efieq1re ( ( 𝐴 ∈ ℂ ∧ ( exp ‘ ( i · 𝐴 ) ) = 1 ) → 𝐴 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 replim ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) = ( i · ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
3 ax-icn ⊢ i ∈ ℂ
4 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
5 4 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
6 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
7 6 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
8 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
9 3 7 8 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
10 adddi ⊢ ( ( i ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) → ( i · ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( i · ( ℜ ‘ 𝐴 ) ) + ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
11 3 5 9 10 mp3an2i ⊢ ( 𝐴 ∈ ℂ → ( i · ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( i · ( ℜ ‘ 𝐴 ) ) + ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
12 ixi ⊢ ( i · i ) = - 1
13 12 oveq1i ⊢ ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( - 1 · ( ℑ ‘ 𝐴 ) )
14 mulass ⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) )
15 3 3 7 14 mp3an12i ⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) )
16 7 mulm1d ⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( ℑ ‘ 𝐴 ) ) = - ( ℑ ‘ 𝐴 ) )
17 13 15 16 3eqtr3a ⊢ ( 𝐴 ∈ ℂ → ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) = - ( ℑ ‘ 𝐴 ) )
18 17 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( i · ( ℜ ‘ 𝐴 ) ) + ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( i · ( ℜ ‘ 𝐴 ) ) + - ( ℑ ‘ 𝐴 ) ) )
19 11 18 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( i · ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( i · ( ℜ ‘ 𝐴 ) ) + - ( ℑ ‘ 𝐴 ) ) )
20 2 19 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) = ( ( i · ( ℜ ‘ 𝐴 ) ) + - ( ℑ ‘ 𝐴 ) ) )
21 20 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( ( i · ( ℜ ‘ 𝐴 ) ) + - ( ℑ ‘ 𝐴 ) ) ) )
22 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℜ ‘ 𝐴 ) ) ∈ ℂ )
23 3 5 22 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( ℜ ‘ 𝐴 ) ) ∈ ℂ )
24 6 renegcld ⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ 𝐴 ) ∈ ℝ )
25 24 recnd ⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ 𝐴 ) ∈ ℂ )
26 efadd ⊢ ( ( ( i · ( ℜ ‘ 𝐴 ) ) ∈ ℂ ∧ - ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · ( ℜ ‘ 𝐴 ) ) + - ( ℑ ‘ 𝐴 ) ) ) = ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) )
27 23 25 26 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · ( ℜ ‘ 𝐴 ) ) + - ( ℑ ‘ 𝐴 ) ) ) = ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) )
28 21 27 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) )
29 28 eqeq1d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) = 1 ↔ ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) = 1 ) )
30 efcl ⊢ ( ( i · ( ℜ ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) ∈ ℂ )
31 23 30 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) ∈ ℂ )
32 efcl ⊢ ( - ( ℑ ‘ 𝐴 ) ∈ ℂ → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
33 25 32 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
34 31 33 absmuld ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) ) = ( ( abs ‘ ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) ) · ( abs ‘ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) ) )
35 absefi ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ℝ → ( abs ‘ ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) ) = 1 )
36 4 35 syl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) ) = 1 )
37 24 reefcld ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
38 efgt0 ⊢ ( - ( ℑ ‘ 𝐴 ) ∈ ℝ → 0 < ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
39 24 38 syl ⊢ ( 𝐴 ∈ ℂ → 0 < ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
40 0re ⊢ 0 ∈ ℝ
41 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( exp ‘ - ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) )
42 40 41 mpan ⊢ ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ∈ ℝ → ( 0 < ( exp ‘ - ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) )
43 37 39 42 sylc ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
44 37 43 absidd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) = ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
45 36 44 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) ) · ( abs ‘ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) ) = ( 1 · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) )
46 33 mulid2d ⊢ ( 𝐴 ∈ ℂ → ( 1 · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) = ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
47 34 45 46 3eqtrrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) ) )
48 fveq2 ⊢ ( ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) = 1 → ( abs ‘ ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) ) = ( abs ‘ 1 ) )
49 47 48 sylan9eq ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) = 1 ) → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ 1 ) )
50 49 ex ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · ( ℜ ‘ 𝐴 ) ) ) · ( exp ‘ - ( ℑ ‘ 𝐴 ) ) ) = 1 → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ 1 ) ) )
51 29 50 sylbid ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) = 1 → ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ 1 ) ) )
52 7 negeq0d ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) = 0 ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
53 reim0b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
54 ef0 ⊢ ( exp ‘ 0 ) = 1
55 abs1 ⊢ ( abs ‘ 1 ) = 1
56 54 55 eqtr4i ⊢ ( exp ‘ 0 ) = ( abs ‘ 1 )
57 56 eqeq2i ⊢ ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ 1 ) )
58 reef11 ⊢ ( ( - ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
59 24 40 58 sylancl ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
60 57 59 bitr3id ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ 1 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
61 52 53 60 3bitr4rd ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( abs ‘ 1 ) ↔ 𝐴 ∈ ℝ ) )
62 51 61 sylibd ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) = 1 → 𝐴 ∈ ℝ ) )
63 62 imp ⊢ ( ( 𝐴 ∈ ℂ ∧ ( exp ‘ ( i · 𝐴 ) ) = 1 ) → 𝐴 ∈ ℝ )