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 tgioo4 ⊢ ( 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 )