Metamath Proof Explorer

Theorem dvlog2

Description: The derivative of the complex logarithm function on the open unit ball centered at 1 , a sometimes easier region to work with than the CC \ ( -oo , 0 ] of dvlog . (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypothesis dvlog2.s 
|- S = ( 1 ( ball ` ( abs o. - ) ) 1 )
Assertion dvlog2 
|- ( CC _D ( log |` S ) ) = ( x e. S |-> ( 1 / x ) )

Proof

Step Hyp Ref Expression
1 dvlog2.s 
 |-  S = ( 1 ( ball ` ( abs o. - ) ) 1 )
2 ssid 
 |-  CC C_ CC
3 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
4 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
5 3 4 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
6 logrncn 
 |-  ( x e. ran log -> x e. CC )
7 6 ssriv 
 |-  ran log C_ CC
8 fss 
 |-  ( ( log : ( CC \ { 0 } ) --> ran log /\ ran log C_ CC ) -> log : ( CC \ { 0 } ) --> CC )
9 5 7 8 mp2an 
 |-  log : ( CC \ { 0 } ) --> CC
10 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
11 10 logdmss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
12 fssres 
 |-  ( ( log : ( CC \ { 0 } ) --> CC /\ ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) ) -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC )
13 9 11 12 mp2an 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC
14 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
15 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
16 ax-1cn 
 |-  1 e. CC
17 1xr 
 |-  1 e. RR*
18 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
19 15 16 17 18 mp3an 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC
20 1 19 eqsstri 
 |-  S C_ CC
21 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
22 21 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
23 22 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
24 21 23 dvres 
 |-  ( ( ( CC C_ CC /\ ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC ) /\ ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ S C_ CC ) ) -> ( CC _D ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) ) = ( ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` S ) ) )
25 2 13 14 20 24 mp4an 
 |-  ( CC _D ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) ) = ( ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` S ) )
26 1 dvlog2lem 
 |-  S C_ ( CC \ ( -oo (,] 0 ) )
27 resabs1 
 |-  ( S C_ ( CC \ ( -oo (,] 0 ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) = ( log |` S ) )
28 26 27 ax-mp 
 |-  ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) = ( log |` S )
29 28 oveq2i 
 |-  ( CC _D ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) |` S ) ) = ( CC _D ( log |` S ) )
30 10 dvlog 
 |-  ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) = ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) )
31 21 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
32 21 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
33 32 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( 1 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) )
34 15 16 17 33 mp3an 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld )
35 1 34 eqeltri 
 |-  S e. ( TopOpen ` CCfld )
36 isopn3i 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S )
37 31 35 36 mp2an 
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S
38 30 37 reseq12i 
 |-  ( ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` S ) ) = ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S )
39 25 29 38 3eqtr3i 
 |-  ( CC _D ( log |` S ) ) = ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S )
40 resmpt 
 |-  ( S C_ ( CC \ ( -oo (,] 0 ) ) -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S ) = ( x e. S |-> ( 1 / x ) ) )
41 26 40 ax-mp 
 |-  ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / x ) ) |` S ) = ( x e. S |-> ( 1 / x ) )
42 39 41 eqtri 
 |-  ( CC _D ( log |` S ) ) = ( x e. S |-> ( 1 / x ) )