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 mnfxr ⊢ -∞ ∈ ℝ*
66 0re ⊢ 0 ∈ ℝ
67 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) ) )
68 65 66 67 mp2an ⊢ ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) )
69 68 bilani ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) )
70 69 simp1d ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ∈ ℝ )
71 0red ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → 0 ∈ ℝ )
72 69 simp3d ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ≤ 0 )
73 efne0 ⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ≠ 0 )
74 57 73 syl ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ≠ 0 )
75 74 adantr ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ≠ 0 )
76 75 necomd ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → 0 ≠ ( exp ‘ 𝑥 ) )
77 70 71 72 76 leneltd ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) < 0 )
78 70 77 negelrpd ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → - ( exp ‘ 𝑥 ) ∈ ℝ+ )
79 lognegb ⊢ ( ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( exp ‘ 𝑥 ) ≠ 0 ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) )
80 56 74 79 syl2anc ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) )
81 80 adantr ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) )
82 78 81 mpbid ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π )
83 64 82 eqtr3d ⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ 𝑥 ) = π )
84 83 ex ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) → ( ℑ ‘ 𝑥 ) = π ) )
85 84 necon3ad ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ( ℑ ‘ 𝑥 ) ≠ π → ¬ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) )
86 62 85 mpd ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ¬ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) )
87 56 86 eldifd ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
88 87 1 eleqtrrdi ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ 𝐷 )
89 funfvima2 ⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) )
90 4 8 89 mp2an ⊢ ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
91 88 90 syl ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) )
92 51 91 eqeltrrd ⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) )
93 92 ssriv ⊢ ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ( log “ 𝐷 )
94 39 93 eqssi ⊢ ( log “ 𝐷 ) = ( ◡ ℑ “ ( - π (,) π ) )
95 imcncf ⊢ ℑ ∈ ( ℂ –cn→ ℝ )
96 ssid ⊢ ℂ ⊆ ℂ
97 ax-resscn ⊢ ℝ ⊆ ℂ
98 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
99 98 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
100 99 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
101 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
102 98 100 101 cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) )
103 96 97 102 mp2an ⊢ ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) )
104 95 103 eleqtri ⊢ ℑ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) )
105 iooretop ⊢ ( - π (,) π ) ∈ ( topGen ‘ ran (,) )
106 cnima ⊢ ( ( ℑ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) ∧ ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ) → ( ◡ ℑ “ ( - π (,) π ) ) ∈ ( TopOpen ‘ ℂfld ) )
107 104 105 106 mp2an ⊢ ( ◡ ℑ “ ( - π (,) π ) ) ∈ ( TopOpen ‘ ℂfld )
108 94 107 eqeltri ⊢ ( log “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld )