Metamath Proof Explorer

Theorem absefib

Description: A complex number is real iff the exponential of its product with _i has absolute value one. (Contributed by NM, 21-Aug-2008)

Ref Expression
Assertion absefib ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 ef0 ⊢ ( exp ‘ 0 ) = 1
2 1 eqeq2i ⊢ ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 )
3 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
4 3 renegcld ⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ 𝐴 ) ∈ ℝ )
5 0re ⊢ 0 ∈ ℝ
6 reef11 ⊢ ( ( - ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
7 4 5 6 sylancl ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = ( exp ‘ 0 ) ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
8 2 7 bitr3id ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
9 3 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
10 9 negeq0d ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) = 0 ↔ - ( ℑ ‘ 𝐴 ) = 0 ) )
11 8 10 bitr4d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
12 ax-icn ⊢ i ∈ ℂ
13 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
14 12 13 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
15 absef ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) )
16 14 15 syl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) )
17 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
18 17 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
19 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
20 12 9 19 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
21 replim ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
22 18 20 21 comraddd ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) )
23 22 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) = ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) )
24 adddi ⊢ ( ( i ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) = ( ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
25 12 20 18 24 mp3an2i ⊢ ( 𝐴 ∈ ℂ → ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) = ( ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
26 ixi ⊢ ( i · i ) = - 1
27 26 oveq1i ⊢ ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( - 1 · ( ℑ ‘ 𝐴 ) )
28 mulass ⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) )
29 12 12 9 28 mp3an12i ⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ℑ ‘ 𝐴 ) ) = ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) )
30 9 mulm1d ⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( ℑ ‘ 𝐴 ) ) = - ( ℑ ‘ 𝐴 ) )
31 27 29 30 3eqtr3a ⊢ ( 𝐴 ∈ ℂ → ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) = - ( ℑ ‘ 𝐴 ) )
32 31 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( i · ( i · ( ℑ ‘ 𝐴 ) ) ) + ( i · ( ℜ ‘ 𝐴 ) ) ) = ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
33 25 32 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( i · ( ( i · ( ℑ ‘ 𝐴 ) ) + ( ℜ ‘ 𝐴 ) ) ) = ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
34 23 33 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) = ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) )
35 34 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) ) )
36 4 17 crred ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( - ( ℑ ‘ 𝐴 ) + ( i · ( ℜ ‘ 𝐴 ) ) ) ) = - ( ℑ ‘ 𝐴 ) )
37 35 36 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( i · 𝐴 ) ) = - ( ℑ ‘ 𝐴 ) )
38 37 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) = ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
39 16 38 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ - ( ℑ ‘ 𝐴 ) ) )
40 39 eqeq1d ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 ↔ ( exp ‘ - ( ℑ ‘ 𝐴 ) ) = 1 ) )
41 reim0b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
42 11 40 41 3bitr4rd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · 𝐴 ) ) ) = 1 ) )