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 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion logcn 
|- ( log |` D ) e. ( D -cn-> CC )

Proof

Step Hyp Ref Expression
1 logcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
3 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
4 2 3 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
5 1 logdmss 
 |-  D C_ ( CC \ { 0 } )
6 fssres 
 |-  ( ( log : ( CC \ { 0 } ) --> ran log /\ D C_ ( CC \ { 0 } ) ) -> ( log |` D ) : D --> ran log )
7 4 5 6 mp2an 
 |-  ( log |` D ) : D --> ran log
8 ffn 
 |-  ( ( log |` D ) : D --> ran log -> ( log |` D ) Fn D )
9 7 8 ax-mp 
 |-  ( log |` D ) Fn D
10 dffn5 
 |-  ( ( log |` D ) Fn D <-> ( log |` D ) = ( x e. D |-> ( ( log |` D ) ` x ) ) )
11 9 10 mpbi 
 |-  ( log |` D ) = ( x e. D |-> ( ( log |` D ) ` x ) )
12 fvres 
 |-  ( x e. D -> ( ( log |` D ) ` x ) = ( log ` x ) )
13 1 ellogdm 
 |-  ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
14 13 simplbi 
 |-  ( x e. D -> x e. CC )
15 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
16 14 15 logcld 
 |-  ( x e. D -> ( log ` x ) e. CC )
17 16 replimd 
 |-  ( x e. D -> ( log ` x ) = ( ( Re ` ( log ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) )
18 relog 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( Re ` ( log ` x ) ) = ( log ` ( abs ` x ) ) )
19 14 15 18 syl2anc 
 |-  ( x e. D -> ( Re ` ( log ` x ) ) = ( log ` ( abs ` x ) ) )
20 14 15 absrpcld 
 |-  ( x e. D -> ( abs ` x ) e. RR+ )
21 20 fvresd 
 |-  ( x e. D -> ( ( log |` RR+ ) ` ( abs ` x ) ) = ( log ` ( abs ` x ) ) )
22 19 21 eqtr4d 
 |-  ( x e. D -> ( Re ` ( log ` x ) ) = ( ( log |` RR+ ) ` ( abs ` x ) ) )
23 22 oveq1d 
 |-  ( x e. D -> ( ( Re ` ( log ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) = ( ( ( log |` RR+ ) ` ( abs ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) )
24 12 17 23 3eqtrd 
 |-  ( x e. D -> ( ( log |` D ) ` x ) = ( ( ( log |` RR+ ) ` ( abs ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) )
25 24 mpteq2ia 
 |-  ( x e. D |-> ( ( log |` D ) ` x ) ) = ( x e. D |-> ( ( ( log |` RR+ ) ` ( abs ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) )
26 11 25 eqtri 
 |-  ( log |` D ) = ( x e. D |-> ( ( ( log |` RR+ ) ` ( abs ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) )
27 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
28 27 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
29 28 a1i 
 |-  ( T. -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
30 27 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
31 14 ssriv 
 |-  D C_ CC
32 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ D C_ CC ) -> ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) )
33 30 31 32 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D )
34 33 a1i 
 |-  ( T. -> ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) )
35 absf 
 |-  abs : CC --> RR
36 fssres 
 |-  ( ( abs : CC --> RR /\ D C_ CC ) -> ( abs |` D ) : D --> RR )
37 35 31 36 mp2an 
 |-  ( abs |` D ) : D --> RR
38 37 a1i 
 |-  ( T. -> ( abs |` D ) : D --> RR )
39 38 feqmptd 
 |-  ( T. -> ( abs |` D ) = ( x e. D |-> ( ( abs |` D ) ` x ) ) )
40 fvres 
 |-  ( x e. D -> ( ( abs |` D ) ` x ) = ( abs ` x ) )
41 40 mpteq2ia 
 |-  ( x e. D |-> ( ( abs |` D ) ` x ) ) = ( x e. D |-> ( abs ` x ) )
42 39 41 eqtrdi 
 |-  ( T. -> ( abs |` D ) = ( x e. D |-> ( abs ` x ) ) )
43 ffn 
 |-  ( ( abs |` D ) : D --> RR -> ( abs |` D ) Fn D )
44 37 43 ax-mp 
 |-  ( abs |` D ) Fn D
45 40 20 eqeltrd 
 |-  ( x e. D -> ( ( abs |` D ) ` x ) e. RR+ )
46 45 rgen 
 |-  A. x e. D ( ( abs |` D ) ` x ) e. RR+
47 ffnfv 
 |-  ( ( abs |` D ) : D --> RR+ <-> ( ( abs |` D ) Fn D /\ A. x e. D ( ( abs |` D ) ` x ) e. RR+ ) )
48 44 46 47 mpbir2an 
 |-  ( abs |` D ) : D --> RR+
49 rpssre 
 |-  RR+ C_ RR
50 ax-resscn 
 |-  RR C_ CC
51 49 50 sstri 
 |-  RR+ C_ CC
52 abscncf 
 |-  abs e. ( CC -cn-> RR )
53 rescncf 
 |-  ( D C_ CC -> ( abs e. ( CC -cn-> RR ) -> ( abs |` D ) e. ( D -cn-> RR ) ) )
54 31 52 53 mp2 
 |-  ( abs |` D ) e. ( D -cn-> RR )
55 cncffvrn 
 |-  ( ( RR+ C_ CC /\ ( abs |` D ) e. ( D -cn-> RR ) ) -> ( ( abs |` D ) e. ( D -cn-> RR+ ) <-> ( abs |` D ) : D --> RR+ ) )
56 51 54 55 mp2an 
 |-  ( ( abs |` D ) e. ( D -cn-> RR+ ) <-> ( abs |` D ) : D --> RR+ )
57 48 56 mpbir 
 |-  ( abs |` D ) e. ( D -cn-> RR+ )
58 42 57 eqeltrrdi 
 |-  ( T. -> ( x e. D |-> ( abs ` x ) ) e. ( D -cn-> RR+ ) )
59 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t D ) = ( ( TopOpen ` CCfld ) |`t D )
60 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t RR+ ) = ( ( TopOpen ` CCfld ) |`t RR+ )
61 27 59 60 cncfcn 
 |-  ( ( D C_ CC /\ RR+ C_ CC ) -> ( D -cn-> RR+ ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( ( TopOpen ` CCfld ) |`t RR+ ) ) )
62 31 51 61 mp2an 
 |-  ( D -cn-> RR+ ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( ( TopOpen ` CCfld ) |`t RR+ ) )
63 58 62 eleqtrdi 
 |-  ( T. -> ( x e. D |-> ( abs ` x ) ) e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( ( TopOpen ` CCfld ) |`t RR+ ) ) )
64 ssid 
 |-  CC C_ CC
65 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR+ -cn-> RR ) C_ ( RR+ -cn-> CC ) )
66 50 64 65 mp2an 
 |-  ( RR+ -cn-> RR ) C_ ( RR+ -cn-> CC )
67 relogcn 
 |-  ( log |` RR+ ) e. ( RR+ -cn-> RR )
68 66 67 sselii 
 |-  ( log |` RR+ ) e. ( RR+ -cn-> CC )
69 68 a1i 
 |-  ( T. -> ( log |` RR+ ) e. ( RR+ -cn-> CC ) )
70 30 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
71 27 60 70 cncfcn 
 |-  ( ( RR+ C_ CC /\ CC C_ CC ) -> ( RR+ -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t RR+ ) Cn ( TopOpen ` CCfld ) ) )
72 51 64 71 mp2an 
 |-  ( RR+ -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t RR+ ) Cn ( TopOpen ` CCfld ) )
73 69 72 eleqtrdi 
 |-  ( T. -> ( log |` RR+ ) e. ( ( ( TopOpen ` CCfld ) |`t RR+ ) Cn ( TopOpen ` CCfld ) ) )
74 34 63 73 cnmpt11f 
 |-  ( T. -> ( x e. D |-> ( ( log |` RR+ ) ` ( abs ` x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
75 27 59 70 cncfcn 
 |-  ( ( D C_ CC /\ CC C_ CC ) -> ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
76 31 64 75 mp2an 
 |-  ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) )
77 74 76 eleqtrrdi 
 |-  ( T. -> ( x e. D |-> ( ( log |` RR+ ) ` ( abs ` x ) ) ) e. ( D -cn-> CC ) )
78 16 imcld 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. RR )
79 78 recnd 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. CC )
80 79 adantl 
 |-  ( ( T. /\ x e. D ) -> ( Im ` ( log ` x ) ) e. CC )
81 eqidd 
 |-  ( T. -> ( x e. D |-> ( Im ` ( log ` x ) ) ) = ( x e. D |-> ( Im ` ( log ` x ) ) ) )
82 eqidd 
 |-  ( T. -> ( y e. CC |-> ( _i x. y ) ) = ( y e. CC |-> ( _i x. y ) ) )
83 oveq2 
 |-  ( y = ( Im ` ( log ` x ) ) -> ( _i x. y ) = ( _i x. ( Im ` ( log ` x ) ) ) )
84 80 81 82 83 fmptco 
 |-  ( T. -> ( ( y e. CC |-> ( _i x. y ) ) o. ( x e. D |-> ( Im ` ( log ` x ) ) ) ) = ( x e. D |-> ( _i x. ( Im ` ( log ` x ) ) ) ) )
85 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( D -cn-> RR ) C_ ( D -cn-> CC ) )
86 50 64 85 mp2an 
 |-  ( D -cn-> RR ) C_ ( D -cn-> CC )
87 1 logcnlem5 
 |-  ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> RR )
88 86 87 sselii 
 |-  ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> CC )
89 88 a1i 
 |-  ( T. -> ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> CC ) )
90 ax-icn 
 |-  _i e. CC
91 eqid 
 |-  ( y e. CC |-> ( _i x. y ) ) = ( y e. CC |-> ( _i x. y ) )
92 91 mulc1cncf 
 |-  ( _i e. CC -> ( y e. CC |-> ( _i x. y ) ) e. ( CC -cn-> CC ) )
93 90 92 mp1i 
 |-  ( T. -> ( y e. CC |-> ( _i x. y ) ) e. ( CC -cn-> CC ) )
94 89 93 cncfco 
 |-  ( T. -> ( ( y e. CC |-> ( _i x. y ) ) o. ( x e. D |-> ( Im ` ( log ` x ) ) ) ) e. ( D -cn-> CC ) )
95 84 94 eqeltrrd 
 |-  ( T. -> ( x e. D |-> ( _i x. ( Im ` ( log ` x ) ) ) ) e. ( D -cn-> CC ) )
96 27 29 77 95 cncfmpt2f 
 |-  ( T. -> ( x e. D |-> ( ( ( log |` RR+ ) ` ( abs ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) ) e. ( D -cn-> CC ) )
97 96 mptru 
 |-  ( x e. D |-> ( ( ( log |` RR+ ) ` ( abs ` x ) ) + ( _i x. ( Im ` ( log ` x ) ) ) ) ) e. ( D -cn-> CC )
98 26 97 eqeltri 
 |-  ( log |` D ) e. ( D -cn-> CC )