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

Metamath Proof Explorer

Theorem cxpcn2

Description: Continuity of the complex power function, when the base is real. (Contributed by Mario Carneiro, 1-May-2016)

Ref Expression
Hypotheses cxpcn2.j 
|- J = ( TopOpen ` CCfld )
cxpcn2.k 
|- K = ( J |`t RR+ )
Assertion cxpcn2 
|- ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 cxpcn2.j 
 |-  J = ( TopOpen ` CCfld )
2 cxpcn2.k 
 |-  K = ( J |`t RR+ )
3 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
4 rpcn 
 |-  ( x e. RR+ -> x e. CC )
5 ax-1 
 |-  ( x e. RR+ -> ( x e. RR -> x e. RR+ ) )
6 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
7 6 ellogdm 
 |-  ( x e. ( CC \ ( -oo (,] 0 ) ) <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
8 4 5 7 sylanbrc 
 |-  ( x e. RR+ -> x e. ( CC \ ( -oo (,] 0 ) ) )
9 8 ssriv 
 |-  RR+ C_ ( CC \ ( -oo (,] 0 ) )
10 cnex 
 |-  CC e. _V
11 10 difexi 
 |-  ( CC \ ( -oo (,] 0 ) ) e. _V
12 restabs 
 |-  ( ( J e. ( TopOn ` CC ) /\ RR+ C_ ( CC \ ( -oo (,] 0 ) ) /\ ( CC \ ( -oo (,] 0 ) ) e. _V ) -> ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) |`t RR+ ) = ( J |`t RR+ ) )
13 3 9 11 12 mp3an 
 |-  ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) |`t RR+ ) = ( J |`t RR+ )
14 2 13 eqtr4i 
 |-  K = ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) |`t RR+ )
15 3 a1i 
 |-  ( T. -> J e. ( TopOn ` CC ) )
16 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
17 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ ( CC \ ( -oo (,] 0 ) ) C_ CC ) -> ( J |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) )
18 15 16 17 sylancl 
 |-  ( T. -> ( J |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) )
19 9 a1i 
 |-  ( T. -> RR+ C_ ( CC \ ( -oo (,] 0 ) ) )
20 3 toponrestid 
 |-  J = ( J |`t CC )
21 ssidd 
 |-  ( T. -> CC C_ CC )
22 eqid 
 |-  ( J |`t ( CC \ ( -oo (,] 0 ) ) ) = ( J |`t ( CC \ ( -oo (,] 0 ) ) )
23 6 1 22 cxpcn 
 |-  ( x e. ( CC \ ( -oo (,] 0 ) ) , y e. CC |-> ( x ^c y ) ) e. ( ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) tX J ) Cn J )
24 23 a1i 
 |-  ( T. -> ( x e. ( CC \ ( -oo (,] 0 ) ) , y e. CC |-> ( x ^c y ) ) e. ( ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) tX J ) Cn J ) )
25 14 18 19 20 15 21 24 cnmpt2res 
 |-  ( T. -> ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J ) )
26 25 mptru 
 |-  ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )