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 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion dvlog 
|- ( CC _D ( log |` D ) ) = ( x e. D |-> ( 1 / x ) )

Proof

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