Metamath Proof Explorer


Theorem logf1o2

Description: The logarithm maps its continuous domain bijectively onto the set of numbers with imaginary part -upi < Im ( z ) < pi . The negative reals are mapped to the numbers with imaginary part equal to _pi . (Contributed by Mario Carneiro, 2-May-2015)

Ref Expression
Hypothesis logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion logf1o2 ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( ℑ “ ( - π (,) π ) )

Proof

Step Hyp Ref Expression
1 logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 logf1o log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
3 f1of1 ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) –1-1→ ran log )
4 2 3 ax-mp log : ( ℂ ∖ { 0 } ) –1-1→ ran log
5 1 logdmss 𝐷 ⊆ ( ℂ ∖ { 0 } )
6 f1ores ( ( log : ( ℂ ∖ { 0 } ) –1-1→ ran log ∧ 𝐷 ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( log “ 𝐷 ) )
7 4 5 6 mp2an ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( log “ 𝐷 )
8 f1ofun ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun log )
9 2 8 ax-mp Fun log
10 f1of ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
11 2 10 ax-mp log : ( ℂ ∖ { 0 } ) ⟶ ran log
12 11 fdmi dom log = ( ℂ ∖ { 0 } )
13 5 12 sseqtrri 𝐷 ⊆ dom log
14 funimass4 ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( log “ 𝐷 ) ⊆ ( ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥𝐷 ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) ) )
15 9 13 14 mp2an ( ( log “ 𝐷 ) ⊆ ( ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥𝐷 ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) )
16 1 ellogdm ( 𝑥𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
17 16 simplbi ( 𝑥𝐷𝑥 ∈ ℂ )
18 1 logdmn0 ( 𝑥𝐷𝑥 ≠ 0 )
19 17 18 logcld ( 𝑥𝐷 → ( log ‘ 𝑥 ) ∈ ℂ )
20 19 imcld ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ )
21 17 18 logimcld ( 𝑥𝐷 → ( - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) )
22 21 simpld ( 𝑥𝐷 → - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) )
23 pire π ∈ ℝ
24 23 a1i ( 𝑥𝐷 → π ∈ ℝ )
25 21 simprd ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π )
26 1 logdmnrp ( 𝑥𝐷 → ¬ - 𝑥 ∈ ℝ+ )
27 lognegb ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) )
28 17 18 27 syl2anc ( 𝑥𝐷 → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) )
29 28 necon3bbid ( 𝑥𝐷 → ( ¬ - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) )
30 26 29 mpbid ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π )
31 30 necomd ( 𝑥𝐷 → π ≠ ( ℑ ‘ ( log ‘ 𝑥 ) ) )
32 20 24 25 31 leneltd ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) < π )
33 23 renegcli - π ∈ ℝ
34 33 rexri - π ∈ ℝ*
35 23 rexri π ∈ ℝ*
36 elioo2 ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) )
37 34 35 36 mp2an ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) )
38 20 22 32 37 syl3anbrc ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) )
39 imf ℑ : ℂ ⟶ ℝ
40 ffn ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ )
41 elpreima ( ℑ Fn ℂ → ( ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) )
42 39 40 41 mp2b ( ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) )
43 19 38 42 sylanbrc ( 𝑥𝐷 → ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) )
44 15 43 mprgbir ( log “ 𝐷 ) ⊆ ( ℑ “ ( - π (,) π ) )
45 elpreima ( ℑ Fn ℂ → ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) )
46 39 40 45 mp2b ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) )
47 simpl ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ℂ )
48 eliooord ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
49 48 adantl ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
50 49 simpld ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → - π < ( ℑ ‘ 𝑥 ) )
51 49 simprd ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) < π )
52 imcl ( 𝑥 ∈ ℂ → ( ℑ ‘ 𝑥 ) ∈ ℝ )
53 52 adantr ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
54 ltle ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) < π → ( ℑ ‘ 𝑥 ) ≤ π ) )
55 53 23 54 sylancl ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ( ℑ ‘ 𝑥 ) < π → ( ℑ ‘ 𝑥 ) ≤ π ) )
56 51 55 mpd ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ≤ π )
57 ellogrn ( 𝑥 ∈ ran log ↔ ( 𝑥 ∈ ℂ ∧ - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) ≤ π ) )
58 47 50 56 57 syl3anbrc ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ran log )
59 logef ( 𝑥 ∈ ran log → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
60 58 59 syl ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
61 efcl ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
62 61 adantr ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ )
63 53 adantr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
64 63 recnd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℂ )
65 picn π ∈ ℂ
66 65 a1i ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ∈ ℂ )
67 pipos 0 < π
68 23 67 gt0ne0ii π ≠ 0
69 68 a1i ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ≠ 0 )
70 51 adantr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) < π )
71 65 mulid1i ( π · 1 ) = π
72 70 71 breqtrrdi ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) < ( π · 1 ) )
73 1re 1 ∈ ℝ
74 73 a1i ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 1 ∈ ℝ )
75 23 a1i ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ∈ ℝ )
76 67 a1i ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 0 < π )
77 ltdivmul ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( ( ℑ ‘ 𝑥 ) / π ) < 1 ↔ ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) )
78 63 74 75 76 77 syl112anc ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) < 1 ↔ ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) )
79 72 78 mpbird ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) < 1 )
80 1e0p1 1 = ( 0 + 1 )
81 79 80 breqtrdi ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) )
82 63 recoscld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( cos ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
83 63 resincld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ )
84 82 83 crimd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) = ( sin ‘ ( ℑ ‘ 𝑥 ) ) )
85 efeul ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) = ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) )
86 85 ad2antrr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) = ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) )
87 86 oveq1d ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) )
88 82 recnd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( cos ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ )
89 ax-icn i ∈ ℂ
90 83 recnd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ )
91 mulcl ( ( i ∈ ℂ ∧ ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ ) → ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ∈ ℂ )
92 89 90 91 sylancr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ∈ ℂ )
93 88 92 addcld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ∈ ℂ )
94 recl ( 𝑥 ∈ ℂ → ( ℜ ‘ 𝑥 ) ∈ ℝ )
95 94 ad2antrr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℜ ‘ 𝑥 ) ∈ ℝ )
96 95 recnd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℜ ‘ 𝑥 ) ∈ ℂ )
97 efcl ( ( ℜ ‘ 𝑥 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℂ )
98 96 97 syl ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℂ )
99 efne0 ( ( ℜ ‘ 𝑥 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ≠ 0 )
100 96 99 syl ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ≠ 0 )
101 93 98 100 divcan3d ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) )
102 87 101 eqtrd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) )
103 simpr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ )
104 95 reefcld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℝ )
105 103 104 100 redivcld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) ∈ ℝ )
106 102 105 eqeltrrd ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ∈ ℝ )
107 106 reim0d ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) = 0 )
108 84 107 eqtr3d ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 )
109 sineq0 ( ( ℑ ‘ 𝑥 ) ∈ ℂ → ( ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) )
110 64 109 syl ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) )
111 108 110 mpbid ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ )
112 0z 0 ∈ ℤ
113 zleltp1 ( ( ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) )
114 111 112 113 sylancl ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) )
115 81 114 mpbird ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 )
116 df-neg - 1 = ( 0 − 1 )
117 65 mulm1i ( - 1 · π ) = - π
118 50 adantr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - π < ( ℑ ‘ 𝑥 ) )
119 117 118 eqbrtrid ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( - 1 · π ) < ( ℑ ‘ 𝑥 ) )
120 73 renegcli - 1 ∈ ℝ
121 120 a1i ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - 1 ∈ ℝ )
122 ltmuldiv ( ( - 1 ∈ ℝ ∧ ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ↔ - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) )
123 121 63 75 76 122 syl112anc ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ↔ - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) )
124 119 123 mpbid ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - 1 < ( ( ℑ ‘ 𝑥 ) / π ) )
125 116 124 eqbrtrrid ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) )
126 zlem1lt ( ( 0 ∈ ℤ ∧ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) → ( 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ↔ ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) )
127 112 111 126 sylancr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ↔ ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) )
128 125 127 mpbird ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) )
129 63 75 69 redivcld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℝ )
130 0re 0 ∈ ℝ
131 letri3 ( ( ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) = 0 ↔ ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ∧ 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) ) )
132 129 130 131 sylancl ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) = 0 ↔ ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ∧ 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) ) )
133 115 128 132 mpbir2and ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) = 0 )
134 64 66 69 133 diveq0d ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) = 0 )
135 reim0b ( 𝑥 ∈ ℂ → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
136 135 ad2antrr ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) )
137 134 136 mpbird ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ∈ ℝ )
138 137 rpefcld ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ+ )
139 138 ex ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ( exp ‘ 𝑥 ) ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ ) )
140 1 ellogdm ( ( exp ‘ 𝑥 ) ∈ 𝐷 ↔ ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( ( exp ‘ 𝑥 ) ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ ) ) )
141 62 139 140 sylanbrc ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ 𝐷 )
142 funfvima2 ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) )
143 9 13 142 mp2an ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
144 141 143 syl ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
145 60 144 eqeltrrd ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) )
146 46 145 sylbi ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) )
147 146 ssriv ( ℑ “ ( - π (,) π ) ) ⊆ ( log “ 𝐷 )
148 44 147 eqssi ( log “ 𝐷 ) = ( ℑ “ ( - π (,) π ) )
149 f1oeq3 ( ( log “ 𝐷 ) = ( ℑ “ ( - π (,) π ) ) → ( ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( log “ 𝐷 ) ↔ ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( ℑ “ ( - π (,) π ) ) ) )
150 148 149 ax-mp ( ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( log “ 𝐷 ) ↔ ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( ℑ “ ( - π (,) π ) ) )
151 7 150 mpbi ( log ↾ 𝐷 ) : 𝐷1-1-onto→ ( ℑ “ ( - π (,) π ) )