Metamath Proof Explorer

Theorem cxpcn

Description: Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016)

Ref Expression
Hypotheses cxpcn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
cxpcn.j 
|- J = ( TopOpen ` CCfld )
cxpcn.k 
|- K = ( J |`t D )
Assertion cxpcn 
|- ( x e. D , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 cxpcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 cxpcn.j 
 |-  J = ( TopOpen ` CCfld )
3 cxpcn.k 
 |-  K = ( J |`t D )
4 1 ellogdm 
 |-  ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
5 4 simplbi 
 |-  ( x e. D -> x e. CC )
6 5 adantr 
 |-  ( ( x e. D /\ y e. CC ) -> x e. CC )
7 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
8 7 adantr 
 |-  ( ( x e. D /\ y e. CC ) -> x =/= 0 )
9 simpr 
 |-  ( ( x e. D /\ y e. CC ) -> y e. CC )
10 6 8 9 cxpefd 
 |-  ( ( x e. D /\ y e. CC ) -> ( x ^c y ) = ( exp ` ( y x. ( log ` x ) ) ) )
11 10 mpoeq3ia 
 |-  ( x e. D , y e. CC |-> ( x ^c y ) ) = ( x e. D , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
12 2 cnfldtopon 
 |-  J e. ( TopOn ` CC )
13 12 a1i 
 |-  ( T. -> J e. ( TopOn ` CC ) )
14 5 ssriv 
 |-  D C_ CC
15 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ D C_ CC ) -> ( J |`t D ) e. ( TopOn ` D ) )
16 13 14 15 sylancl 
 |-  ( T. -> ( J |`t D ) e. ( TopOn ` D ) )
17 3 16 eqeltrid 
 |-  ( T. -> K e. ( TopOn ` D ) )
18 17 13 cnmpt2nd 
 |-  ( T. -> ( x e. D , y e. CC |-> y ) e. ( ( K tX J ) Cn J ) )
19 fvres 
 |-  ( x e. D -> ( ( log |` D ) ` x ) = ( log ` x ) )
20 19 adantr 
 |-  ( ( x e. D /\ y e. CC ) -> ( ( log |` D ) ` x ) = ( log ` x ) )
21 20 mpoeq3ia 
 |-  ( x e. D , y e. CC |-> ( ( log |` D ) ` x ) ) = ( x e. D , y e. CC |-> ( log ` x ) )
22 17 13 cnmpt1st 
 |-  ( T. -> ( x e. D , y e. CC |-> x ) e. ( ( K tX J ) Cn K ) )
23 1 logcn 
 |-  ( log |` D ) e. ( D -cn-> CC )
24 ssid 
 |-  CC C_ CC
25 12 toponrestid 
 |-  J = ( J |`t CC )
26 2 3 25 cncfcn 
 |-  ( ( D C_ CC /\ CC C_ CC ) -> ( D -cn-> CC ) = ( K Cn J ) )
27 14 24 26 mp2an 
 |-  ( D -cn-> CC ) = ( K Cn J )
28 23 27 eleqtri 
 |-  ( log |` D ) e. ( K Cn J )
29 28 a1i 
 |-  ( T. -> ( log |` D ) e. ( K Cn J ) )
30 17 13 22 29 cnmpt21f 
 |-  ( T. -> ( x e. D , y e. CC |-> ( ( log |` D ) ` x ) ) e. ( ( K tX J ) Cn J ) )
31 21 30 eqeltrrid 
 |-  ( T. -> ( x e. D , y e. CC |-> ( log ` x ) ) e. ( ( K tX J ) Cn J ) )
32 2 mulcn 
 |-  x. e. ( ( J tX J ) Cn J )
33 32 a1i 
 |-  ( T. -> x. e. ( ( J tX J ) Cn J ) )
34 17 13 18 31 33 cnmpt22f 
 |-  ( T. -> ( x e. D , y e. CC |-> ( y x. ( log ` x ) ) ) e. ( ( K tX J ) Cn J ) )
35 efcn 
 |-  exp e. ( CC -cn-> CC )
36 2 cncfcn1 
 |-  ( CC -cn-> CC ) = ( J Cn J )
37 35 36 eleqtri 
 |-  exp e. ( J Cn J )
38 37 a1i 
 |-  ( T. -> exp e. ( J Cn J ) )
39 17 13 34 38 cnmpt21f 
 |-  ( T. -> ( x e. D , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) ) e. ( ( K tX J ) Cn J ) )
40 39 mptru 
 |-  ( x e. D , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) ) e. ( ( K tX J ) Cn J )
41 11 40 eqeltri 
 |-  ( x e. D , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )