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 ) → 𝐴 ∈ ℝ )