Metamath Proof Explorer

Theorem dvlog

Description: The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypothesis logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion dvlog ( ℂ D ( log ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )

Proof

Step Hyp Ref Expression
1 logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 2 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
4 3 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
5 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
6 5 a1i ⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
7 1 logdmopn ⊢ 𝐷 ∈ ( TopOpen ‘ ℂfld )
8 7 a1i ⊢ ( ⊤ → 𝐷 ∈ ( TopOpen ‘ ℂfld ) )
9 logf1o ⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
10 f1of1 ⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) –1-1→ ran log )
11 9 10 ax-mp ⊢ log : ( ℂ ∖ { 0 } ) –1-1→ ran log
12 1 logdmss ⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } )
13 f1ores ⊢ ( ( log : ( ℂ ∖ { 0 } ) –1-1→ ran log ∧ 𝐷 ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) )
14 11 12 13 mp2an ⊢ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 )
15 f1ocnv ⊢ ( ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) → ◡ ( log ↾ 𝐷 ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 )
16 14 15 ax-mp ⊢ ◡ ( log ↾ 𝐷 ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷
17 df-log ⊢ log = ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) )
18 17 reseq1i ⊢ ( log ↾ 𝐷 ) = ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ 𝐷 )
19 18 cnveqi ⊢ ◡ ( log ↾ 𝐷 ) = ◡ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ 𝐷 )
20 eff ⊢ exp : ℂ ⟶ ℂ
21 cnvimass ⊢ ( ◡ ℑ “ ( - π (,] π ) ) ⊆ dom ℑ
22 imf ⊢ ℑ : ℂ ⟶ ℝ
23 22 fdmi ⊢ dom ℑ = ℂ
24 21 23 sseqtri ⊢ ( ◡ ℑ “ ( - π (,] π ) ) ⊆ ℂ
25 fssres ⊢ ( ( exp : ℂ ⟶ ℂ ∧ ( ◡ ℑ “ ( - π (,] π ) ) ⊆ ℂ ) → ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ◡ ℑ “ ( - π (,] π ) ) ⟶ ℂ )
26 20 24 25 mp2an ⊢ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ◡ ℑ “ ( - π (,] π ) ) ⟶ ℂ
27 ffun ⊢ ( ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ◡ ℑ “ ( - π (,] π ) ) ⟶ ℂ → Fun ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) )
28 funcnvres2 ⊢ ( Fun ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) → ◡ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ 𝐷 ) = ( ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ) )
29 26 27 28 mp2b ⊢ ◡ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ 𝐷 ) = ( ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) )
30 cnvimass ⊢ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ⊆ dom ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) )
31 26 fdmi ⊢ dom ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) = ( ◡ ℑ “ ( - π (,] π ) )
32 30 31 sseqtri ⊢ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,] π ) )
33 resabs1 ⊢ ( ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,] π ) ) → ( ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ) = ( exp ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ) )
34 32 33 ax-mp ⊢ ( ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) ) = ( exp ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) )
35 19 29 34 3eqtri ⊢ ◡ ( log ↾ 𝐷 ) = ( exp ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) )
36 17 imaeq1i ⊢ ( log “ 𝐷 ) = ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 )
37 36 reseq2i ⊢ ( exp ↾ ( log “ 𝐷 ) ) = ( exp ↾ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) “ 𝐷 ) )
38 35 37 eqtr4i ⊢ ◡ ( log ↾ 𝐷 ) = ( exp ↾ ( log “ 𝐷 ) )
39 f1oeq1 ⊢ ( ◡ ( log ↾ 𝐷 ) = ( exp ↾ ( log “ 𝐷 ) ) → ( ◡ ( log ↾ 𝐷 ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 ↔ ( exp ↾ ( log “ 𝐷 ) ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 ) )
40 38 39 ax-mp ⊢ ( ◡ ( log ↾ 𝐷 ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 ↔ ( exp ↾ ( log “ 𝐷 ) ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 )
41 16 40 mpbi ⊢ ( exp ↾ ( log “ 𝐷 ) ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷
42 41 a1i ⊢ ( ⊤ → ( exp ↾ ( log “ 𝐷 ) ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 )
43 38 cnveqi ⊢ ◡ ◡ ( log ↾ 𝐷 ) = ◡ ( exp ↾ ( log “ 𝐷 ) )
44 relres ⊢ Rel ( log ↾ 𝐷 )
45 dfrel2 ⊢ ( Rel ( log ↾ 𝐷 ) ↔ ◡ ◡ ( log ↾ 𝐷 ) = ( log ↾ 𝐷 ) )
46 44 45 mpbi ⊢ ◡ ◡ ( log ↾ 𝐷 ) = ( log ↾ 𝐷 )
47 43 46 eqtr3i ⊢ ◡ ( exp ↾ ( log “ 𝐷 ) ) = ( log ↾ 𝐷 )
48 f1of ⊢ ( ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) → ( log ↾ 𝐷 ) : 𝐷 ⟶ ( log “ 𝐷 ) )
49 14 48 mp1i ⊢ ( ⊤ → ( log ↾ 𝐷 ) : 𝐷 ⟶ ( log “ 𝐷 ) )
50 imassrn ⊢ ( log “ 𝐷 ) ⊆ ran log
51 logrncn ⊢ ( 𝑥 ∈ ran log → 𝑥 ∈ ℂ )
52 51 ssriv ⊢ ran log ⊆ ℂ
53 50 52 sstri ⊢ ( log “ 𝐷 ) ⊆ ℂ
54 1 logcn ⊢ ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )
55 cncffvrn ⊢ ( ( ( log “ 𝐷 ) ⊆ ℂ ∧ ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ ) ) → ( ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ( log “ 𝐷 ) ) ↔ ( log ↾ 𝐷 ) : 𝐷 ⟶ ( log “ 𝐷 ) ) )
56 53 54 55 mp2an ⊢ ( ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ( log “ 𝐷 ) ) ↔ ( log ↾ 𝐷 ) : 𝐷 ⟶ ( log “ 𝐷 ) )
57 49 56 sylibr ⊢ ( ⊤ → ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ( log “ 𝐷 ) ) )
58 47 57 eqeltrid ⊢ ( ⊤ → ◡ ( exp ↾ ( log “ 𝐷 ) ) ∈ ( 𝐷 –cn→ ( log “ 𝐷 ) ) )
59 ssid ⊢ ℂ ⊆ ℂ
60 2 4 dvres ⊢ ( ( ( ℂ ⊆ ℂ ∧ exp : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ( log “ 𝐷 ) ⊆ ℂ ) ) → ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) = ( ( ℂ D exp ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( log “ 𝐷 ) ) ) )
61 59 20 59 53 60 mp4an ⊢ ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) = ( ( ℂ D exp ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( log “ 𝐷 ) ) )
62 dvef ⊢ ( ℂ D exp ) = exp
63 2 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
64 1 dvloglem ⊢ ( log “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld )
65 isopn3i ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( log “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( log “ 𝐷 ) ) = ( log “ 𝐷 ) )
66 63 64 65 mp2an ⊢ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( log “ 𝐷 ) ) = ( log “ 𝐷 )
67 62 66 reseq12i ⊢ ( ( ℂ D exp ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( log “ 𝐷 ) ) ) = ( exp ↾ ( log “ 𝐷 ) )
68 61 67 eqtri ⊢ ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) = ( exp ↾ ( log “ 𝐷 ) )
69 68 dmeqi ⊢ dom ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) = dom ( exp ↾ ( log “ 𝐷 ) )
70 dmres ⊢ dom ( exp ↾ ( log “ 𝐷 ) ) = ( ( log “ 𝐷 ) ∩ dom exp )
71 20 fdmi ⊢ dom exp = ℂ
72 53 71 sseqtrri ⊢ ( log “ 𝐷 ) ⊆ dom exp
73 df-ss ⊢ ( ( log “ 𝐷 ) ⊆ dom exp ↔ ( ( log “ 𝐷 ) ∩ dom exp ) = ( log “ 𝐷 ) )
74 72 73 mpbi ⊢ ( ( log “ 𝐷 ) ∩ dom exp ) = ( log “ 𝐷 )
75 69 70 74 3eqtri ⊢ dom ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) = ( log “ 𝐷 )
76 75 a1i ⊢ ( ⊤ → dom ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) = ( log “ 𝐷 ) )
77 neirr ⊢ ¬ 0 ≠ 0
78 resss ⊢ ( ( ℂ D exp ) ↾ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( log “ 𝐷 ) ) ) ⊆ ( ℂ D exp )
79 61 78 eqsstri ⊢ ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ⊆ ( ℂ D exp )
80 79 62 sseqtri ⊢ ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ⊆ exp
81 80 rnssi ⊢ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ⊆ ran exp
82 eff2 ⊢ exp : ℂ ⟶ ( ℂ ∖ { 0 } )
83 frn ⊢ ( exp : ℂ ⟶ ( ℂ ∖ { 0 } ) → ran exp ⊆ ( ℂ ∖ { 0 } ) )
84 82 83 ax-mp ⊢ ran exp ⊆ ( ℂ ∖ { 0 } )
85 81 84 sstri ⊢ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ⊆ ( ℂ ∖ { 0 } )
86 85 sseli ⊢ ( 0 ∈ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) → 0 ∈ ( ℂ ∖ { 0 } ) )
87 eldifsn ⊢ ( 0 ∈ ( ℂ ∖ { 0 } ) ↔ ( 0 ∈ ℂ ∧ 0 ≠ 0 ) )
88 86 87 sylib ⊢ ( 0 ∈ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) → ( 0 ∈ ℂ ∧ 0 ≠ 0 ) )
89 88 simprd ⊢ ( 0 ∈ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) → 0 ≠ 0 )
90 77 89 mto ⊢ ¬ 0 ∈ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) )
91 90 a1i ⊢ ( ⊤ → ¬ 0 ∈ ran ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) )
92 2 4 6 8 42 58 76 91 dvcnv ⊢ ( ⊤ → ( ℂ D ◡ ( exp ↾ ( log “ 𝐷 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) ) ) )
93 92 mptru ⊢ ( ℂ D ◡ ( exp ↾ ( log “ 𝐷 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) ) )
94 47 oveq2i ⊢ ( ℂ D ◡ ( exp ↾ ( log “ 𝐷 ) ) ) = ( ℂ D ( log ↾ 𝐷 ) )
95 68 fveq1i ⊢ ( ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) = ( ( exp ↾ ( log “ 𝐷 ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) )
96 f1ocnvfv2 ⊢ ( ( ( exp ↾ ( log “ 𝐷 ) ) : ( log “ 𝐷 ) –1-1-onto→ 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ( exp ↾ ( log “ 𝐷 ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) = 𝑥 )
97 41 96 mpan ⊢ ( 𝑥 ∈ 𝐷 → ( ( exp ↾ ( log “ 𝐷 ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) = 𝑥 )
98 95 97 syl5eq ⊢ ( 𝑥 ∈ 𝐷 → ( ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) = 𝑥 )
99 98 oveq2d ⊢ ( 𝑥 ∈ 𝐷 → ( 1 / ( ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) ) = ( 1 / 𝑥 ) )
100 99 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( ( ℂ D ( exp ↾ ( log “ 𝐷 ) ) ) ‘ ( ◡ ( exp ↾ ( log “ 𝐷 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )
101 93 94 100 3eqtr3i ⊢ ( ℂ D ( log ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )