Metamath Proof Explorer


Theorem dvloglem

Description: Lemma for dvlog . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypothesis logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion dvloglem ( log “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 logf1o log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
3 f1ofun ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun log )
4 2 3 ax-mp Fun log
5 1 logdmss 𝐷 ⊆ ( ℂ ∖ { 0 } )
6 f1odm ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → dom log = ( ℂ ∖ { 0 } ) )
7 2 6 ax-mp dom log = ( ℂ ∖ { 0 } )
8 5 7 sseqtrri 𝐷 ⊆ dom log
9 funimass4 ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( log “ 𝐷 ) ⊆ ( ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥𝐷 ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) ) )
10 4 8 9 mp2an ( ( log “ 𝐷 ) ⊆ ( ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥𝐷 ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) )
11 1 ellogdm ( 𝑥𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
12 11 simplbi ( 𝑥𝐷𝑥 ∈ ℂ )
13 1 logdmn0 ( 𝑥𝐷𝑥 ≠ 0 )
14 12 13 logcld ( 𝑥𝐷 → ( log ‘ 𝑥 ) ∈ ℂ )
15 14 imcld ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ )
16 12 13 logimcld ( 𝑥𝐷 → ( - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) )
17 16 simpld ( 𝑥𝐷 → - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) )
18 pire π ∈ ℝ
19 18 a1i ( 𝑥𝐷 → π ∈ ℝ )
20 16 simprd ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π )
21 1 logdmnrp ( 𝑥𝐷 → ¬ - 𝑥 ∈ ℝ+ )
22 lognegb ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) )
23 12 13 22 syl2anc ( 𝑥𝐷 → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) )
24 23 necon3bbid ( 𝑥𝐷 → ( ¬ - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) )
25 21 24 mpbid ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π )
26 25 necomd ( 𝑥𝐷 → π ≠ ( ℑ ‘ ( log ‘ 𝑥 ) ) )
27 15 19 20 26 leneltd ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) < π )
28 18 renegcli - π ∈ ℝ
29 28 rexri - π ∈ ℝ*
30 18 rexri π ∈ ℝ*
31 elioo2 ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) )
32 29 30 31 mp2an ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) )
33 15 17 27 32 syl3anbrc ( 𝑥𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) )
34 imf ℑ : ℂ ⟶ ℝ
35 ffn ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ )
36 elpreima ( ℑ Fn ℂ → ( ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) )
37 34 35 36 mp2b ( ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) )
38 14 33 37 sylanbrc ( 𝑥𝐷 → ( log ‘ 𝑥 ) ∈ ( ℑ “ ( - π (,) π ) ) )
39 10 38 mprgbir ( log “ 𝐷 ) ⊆ ( ℑ “ ( - π (,) π ) )
40 df-ioo (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )
41 df-ioc (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧𝑦 ) } )
42 idd ( ( - π ∈ ℝ*𝑤 ∈ ℝ* ) → ( - π < 𝑤 → - π < 𝑤 ) )
43 xrltle ( ( 𝑤 ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝑤 < π → 𝑤 ≤ π ) )
44 40 41 42 43 ixxssixx ( - π (,) π ) ⊆ ( - π (,] π )
45 imass2 ( ( - π (,) π ) ⊆ ( - π (,] π ) → ( ℑ “ ( - π (,) π ) ) ⊆ ( ℑ “ ( - π (,] π ) ) )
46 44 45 ax-mp ( ℑ “ ( - π (,) π ) ) ⊆ ( ℑ “ ( - π (,] π ) )
47 logrn ran log = ( ℑ “ ( - π (,] π ) )
48 46 47 sseqtrri ( ℑ “ ( - π (,) π ) ) ⊆ ran log
49 48 sseli ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ran log )
50 logef ( 𝑥 ∈ ran log → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
51 49 50 syl ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
52 elpreima ( ℑ Fn ℂ → ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) )
53 34 35 52 mp2b ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) )
54 efcl ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
55 54 adantr ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ )
56 53 55 sylbi ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ )
57 53 simplbi ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ℂ )
58 57 imcld ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ )
59 eliooord ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
60 53 59 simplbiim ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) )
61 60 simprd ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) < π )
62 58 61 ltned ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ≠ π )
63 51 adantr ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 )
64 63 fveq2d ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = ( ℑ ‘ 𝑥 ) )
65 simpr ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) )
66 mnfxr -∞ ∈ ℝ*
67 0re 0 ∈ ℝ
68 elioc2 ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) ) )
69 66 67 68 mp2an ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) )
70 65 69 sylib ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) )
71 70 simp1d ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ∈ ℝ )
72 0red ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → 0 ∈ ℝ )
73 70 simp3d ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ≤ 0 )
74 efne0 ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ≠ 0 )
75 57 74 syl ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ≠ 0 )
76 75 adantr ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ≠ 0 )
77 76 necomd ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → 0 ≠ ( exp ‘ 𝑥 ) )
78 71 72 73 77 leneltd ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) < 0 )
79 71 78 negelrpd ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → - ( exp ‘ 𝑥 ) ∈ ℝ+ )
80 lognegb ( ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( exp ‘ 𝑥 ) ≠ 0 ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) )
81 56 75 80 syl2anc ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) )
82 81 adantr ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) )
83 79 82 mpbid ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π )
84 64 83 eqtr3d ( ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ 𝑥 ) = π )
85 84 ex ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) → ( ℑ ‘ 𝑥 ) = π ) )
86 85 necon3ad ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( ( ℑ ‘ 𝑥 ) ≠ π → ¬ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) )
87 62 86 mpd ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ¬ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) )
88 56 87 eldifd ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
89 88 1 eleqtrrdi ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ 𝐷 )
90 funfvima2 ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) )
91 4 8 90 mp2an ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
92 89 91 syl ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
93 51 92 eqeltrrd ( 𝑥 ∈ ( ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) )
94 93 ssriv ( ℑ “ ( - π (,) π ) ) ⊆ ( log “ 𝐷 )
95 39 94 eqssi ( log “ 𝐷 ) = ( ℑ “ ( - π (,) π ) )
96 imcncf ℑ ∈ ( ℂ –cn→ ℝ )
97 ssid ℂ ⊆ ℂ
98 ax-resscn ℝ ⊆ ℂ
99 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
100 99 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
101 100 toponrestid ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
102 99 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
103 99 101 102 cncfcn ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) )
104 97 98 103 mp2an ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) )
105 96 104 eleqtri ℑ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) )
106 iooretop ( - π (,) π ) ∈ ( topGen ‘ ran (,) )
107 cnima ( ( ℑ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) ∧ ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ) → ( ℑ “ ( - π (,) π ) ) ∈ ( TopOpen ‘ ℂfld ) )
108 105 106 107 mp2an ( ℑ “ ( - π (,) π ) ) ∈ ( TopOpen ‘ ℂfld )
109 95 108 eqeltri ( log “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld )