This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxpcn

Description: Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J )
33 32 a1i 
 |-  ( T. -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J ) )
34 oveq12 
 |-  ( ( u = y /\ v = ( log ` x ) ) -> ( u x. v ) = ( y x. ( log ` x ) ) )
35 17 13 18 31 13 13 33 34 cnmpt22 
 |-  ( T. -> ( x e. D , y e. CC |-> ( y x. ( log ` x ) ) ) e. ( ( K tX J ) Cn J ) )
36 efcn 
 |-  exp e. ( CC -cn-> CC )
37 2 cncfcn1 
 |-  ( CC -cn-> CC ) = ( J Cn J )
38 36 37 eleqtri 
 |-  exp e. ( J Cn J )
39 38 a1i 
 |-  ( T. -> exp e. ( J Cn J ) )
40 17 13 35 39 cnmpt21f 
 |-  ( T. -> ( x e. D , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) ) e. ( ( K tX J ) Cn J ) )
41 40 mptru 
 |-  ( x e. D , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) ) e. ( ( K tX J ) Cn J )
42 11 41 eqeltri 
 |-  ( x e. D , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )