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 mulridi ⊢ ( π · 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→ ( ◡ ℑ “ ( - π (,) π ) )