Metamath Proof Explorer

Theorem logcn

Description: The logarithm function is continuous away from the branch cut at negative reals. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypothesis logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion logcn ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )

Proof

Step Hyp Ref Expression
1 logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 logf1o ⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
3 f1of ⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
4 2 3 ax-mp ⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log
5 1 logdmss ⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } )
6 fssres ⊢ ( ( log : ( ℂ ∖ { 0 } ) ⟶ ran log ∧ 𝐷 ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ 𝐷 ) : 𝐷 ⟶ ran log )
7 4 5 6 mp2an ⊢ ( log ↾ 𝐷 ) : 𝐷 ⟶ ran log
8 ffn ⊢ ( ( log ↾ 𝐷 ) : 𝐷 ⟶ ran log → ( log ↾ 𝐷 ) Fn 𝐷 )
9 7 8 ax-mp ⊢ ( log ↾ 𝐷 ) Fn 𝐷
10 dffn5 ⊢ ( ( log ↾ 𝐷 ) Fn 𝐷 ↔ ( log ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) )
11 9 10 mpbi ⊢ ( log ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) )
12 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
13 1 ellogdm ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
14 13 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
15 1 logdmn0 ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
16 14 15 logcld ⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ℂ )
17 16 replimd ⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) = ( ( ℜ ‘ ( log ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) )
18 relog ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝑥 ) ) = ( log ‘ ( abs ‘ 𝑥 ) ) )
19 14 15 18 syl2anc ⊢ ( 𝑥 ∈ 𝐷 → ( ℜ ‘ ( log ‘ 𝑥 ) ) = ( log ‘ ( abs ‘ 𝑥 ) ) )
20 14 15 absrpcld ⊢ ( 𝑥 ∈ 𝐷 → ( abs ‘ 𝑥 ) ∈ ℝ+ )
21 20 fvresd ⊢ ( 𝑥 ∈ 𝐷 → ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) = ( log ‘ ( abs ‘ 𝑥 ) ) )
22 19 21 eqtr4d ⊢ ( 𝑥 ∈ 𝐷 → ( ℜ ‘ ( log ‘ 𝑥 ) ) = ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) )
23 22 oveq1d ⊢ ( 𝑥 ∈ 𝐷 → ( ( ℜ ‘ ( log ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) = ( ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) )
24 12 17 23 3eqtrd ⊢ ( 𝑥 ∈ 𝐷 → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) )
25 24 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) )
26 11 25 eqtri ⊢ ( log ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) )
27 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
28 27 addcn ⊢ + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
29 28 a1i ⊢ ( ⊤ → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
30 27 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
31 14 ssriv ⊢ 𝐷 ⊆ ℂ
32 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
33 30 31 32 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 )
34 33 a1i ⊢ ( ⊤ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
35 absf ⊢ abs : ℂ ⟶ ℝ
36 fssres ⊢ ( ( abs : ℂ ⟶ ℝ ∧ 𝐷 ⊆ ℂ ) → ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ )
37 35 31 36 mp2an ⊢ ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ
38 37 a1i ⊢ ( ⊤ → ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ )
39 38 feqmptd ⊢ ( ⊤ → ( abs ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( abs ↾ 𝐷 ) ‘ 𝑥 ) ) )
40 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( abs ↾ 𝐷 ) ‘ 𝑥 ) = ( abs ‘ 𝑥 ) )
41 40 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( abs ↾ 𝐷 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) )
42 39 41 eqtrdi ⊢ ( ⊤ → ( abs ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) )
43 ffn ⊢ ( ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ → ( abs ↾ 𝐷 ) Fn 𝐷 )
44 37 43 ax-mp ⊢ ( abs ↾ 𝐷 ) Fn 𝐷
45 40 20 eqeltrd ⊢ ( 𝑥 ∈ 𝐷 → ( ( abs ↾ 𝐷 ) ‘ 𝑥 ) ∈ ℝ+ )
46 45 rgen ⊢ ∀ 𝑥 ∈ 𝐷 ( ( abs ↾ 𝐷 ) ‘ 𝑥 ) ∈ ℝ+
47 ffnfv ⊢ ( ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ+ ↔ ( ( abs ↾ 𝐷 ) Fn 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ( ( abs ↾ 𝐷 ) ‘ 𝑥 ) ∈ ℝ+ ) )
48 44 46 47 mpbir2an ⊢ ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ+
49 rpssre ⊢ ℝ+ ⊆ ℝ
50 ax-resscn ⊢ ℝ ⊆ ℂ
51 49 50 sstri ⊢ ℝ+ ⊆ ℂ
52 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
53 rescncf ⊢ ( 𝐷 ⊆ ℂ → ( abs ∈ ( ℂ –cn→ ℝ ) → ( abs ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℝ ) ) )
54 31 52 53 mp2 ⊢ ( abs ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℝ )
55 cncffvrn ⊢ ( ( ℝ+ ⊆ ℂ ∧ ( abs ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℝ ) ) → ( ( abs ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℝ+ ) ↔ ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ+ ) )
56 51 54 55 mp2an ⊢ ( ( abs ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℝ+ ) ↔ ( abs ↾ 𝐷 ) : 𝐷 ⟶ ℝ+ )
57 48 56 mpbir ⊢ ( abs ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℝ+ )
58 42 57 eqeltrrdi ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ∈ ( 𝐷 –cn→ ℝ+ ) )
59 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 )
60 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ )
61 27 59 60 cncfcn ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℝ+ ⊆ ℂ ) → ( 𝐷 –cn→ ℝ+ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) ) )
62 31 51 61 mp2an ⊢ ( 𝐷 –cn→ ℝ+ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) )
63 58 62 eleqtrdi ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) ) )
64 ssid ⊢ ℂ ⊆ ℂ
65 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ+ –cn→ ℝ ) ⊆ ( ℝ+ –cn→ ℂ ) )
66 50 64 65 mp2an ⊢ ( ℝ+ –cn→ ℝ ) ⊆ ( ℝ+ –cn→ ℂ )
67 relogcn ⊢ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ )
68 66 67 sselii ⊢ ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ )
69 68 a1i ⊢ ( ⊤ → ( log ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℂ ) )
70 30 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
71 27 60 70 cncfcn ⊢ ( ( ℝ+ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ+ –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( TopOpen ‘ ℂfld ) ) )
72 51 64 71 mp2an ⊢ ( ℝ+ –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( TopOpen ‘ ℂfld ) )
73 69 72 eleqtrdi ⊢ ( ⊤ → ( log ↾ ℝ+ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ+ ) Cn ( TopOpen ‘ ℂfld ) ) )
74 34 63 73 cnmpt11f ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
75 27 59 70 cncfcn ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
76 31 64 75 mp2an ⊢ ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) )
77 74 76 eleqtrrdi ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℂ ) )
78 16 imcld ⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ )
79 78 recnd ⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℂ )
80 79 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℂ )
81 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) )
82 eqidd ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) )
83 oveq2 ⊢ ( 𝑦 = ( ℑ ‘ ( log ‘ 𝑥 ) ) → ( i · 𝑦 ) = ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) )
84 80 81 82 83 fmptco ⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) ∘ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) )
85 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐷 –cn→ ℝ ) ⊆ ( 𝐷 –cn→ ℂ ) )
86 50 64 85 mp2an ⊢ ( 𝐷 –cn→ ℝ ) ⊆ ( 𝐷 –cn→ ℂ )
87 1 logcnlem5 ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℝ )
88 86 87 sselii ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℂ )
89 88 a1i ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ∈ ( 𝐷 –cn→ ℂ ) )
90 ax-icn ⊢ i ∈ ℂ
91 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) )
92 91 mulc1cncf ⊢ ( i ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) )
93 90 92 mp1i ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) )
94 89 93 cncfco ⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( i · 𝑦 ) ) ∘ ( 𝑥 ∈ 𝐷 ↦ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) ∈ ( 𝐷 –cn→ ℂ ) )
95 84 94 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) ∈ ( 𝐷 –cn→ ℂ ) )
96 27 29 77 95 cncfmpt2f ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) ) ∈ ( 𝐷 –cn→ ℂ ) )
97 96 mptru ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( ( log ↾ ℝ+ ) ‘ ( abs ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝑥 ) ) ) ) ) ∈ ( 𝐷 –cn→ ℂ )
98 26 97 eqeltri ⊢ ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )