Metamath Proof Explorer

Theorem cxpcn3

Description: Extend continuity of the complex power function to a base of zero, as long as the exponent has strictly positive real part. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses cxpcn3.d 
|- D = ( `' Re " RR+ )
cxpcn3.j 
|- J = ( TopOpen ` CCfld )
cxpcn3.k 
|- K = ( J |`t ( 0 [,) +oo ) )
cxpcn3.l 
|- L = ( J |`t D )
Assertion cxpcn3 
|- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J )

Proof

Step Hyp Ref Expression
1 cxpcn3.d 
 |-  D = ( `' Re " RR+ )
2 cxpcn3.j 
 |-  J = ( TopOpen ` CCfld )
3 cxpcn3.k 
 |-  K = ( J |`t ( 0 [,) +oo ) )
4 cxpcn3.l 
 |-  L = ( J |`t D )
5 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
6 ax-resscn 
 |-  RR C_ CC
7 5 6 sstri 
 |-  ( 0 [,) +oo ) C_ CC
8 7 sseli 
 |-  ( x e. ( 0 [,) +oo ) -> x e. CC )
9 cnvimass 
 |-  ( `' Re " RR+ ) C_ dom Re
10 ref 
 |-  Re : CC --> RR
11 10 fdmi 
 |-  dom Re = CC
12 9 11 sseqtri 
 |-  ( `' Re " RR+ ) C_ CC
13 1 12 eqsstri 
 |-  D C_ CC
14 13 sseli 
 |-  ( y e. D -> y e. CC )
15 cxpcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ^c y ) e. CC )
16 8 14 15 syl2an 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. D ) -> ( x ^c y ) e. CC )
17 16 rgen2 
 |-  A. x e. ( 0 [,) +oo ) A. y e. D ( x ^c y ) e. CC
18 eqid 
 |-  ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) = ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) )
19 18 fmpo 
 |-  ( A. x e. ( 0 [,) +oo ) A. y e. D ( x ^c y ) e. CC <-> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC )
20 17 19 mpbi 
 |-  ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC
21 2 cnfldtopon 
 |-  J e. ( TopOn ` CC )
22 rpre 
 |-  ( x e. RR+ -> x e. RR )
23 rpge0 
 |-  ( x e. RR+ -> 0 <_ x )
24 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
25 22 23 24 sylanbrc 
 |-  ( x e. RR+ -> x e. ( 0 [,) +oo ) )
26 25 ssriv 
 |-  RR+ C_ ( 0 [,) +oo )
27 26 7 sstri 
 |-  RR+ C_ CC
28 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ RR+ C_ CC ) -> ( J |`t RR+ ) e. ( TopOn ` RR+ ) )
29 21 27 28 mp2an 
 |-  ( J |`t RR+ ) e. ( TopOn ` RR+ )
30 29 toponrestid 
 |-  ( J |`t RR+ ) = ( ( J |`t RR+ ) |`t RR+ )
31 29 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( J |`t RR+ ) e. ( TopOn ` RR+ ) )
32 ssid 
 |-  RR+ C_ RR+
33 32 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> RR+ C_ RR+ )
34 21 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> J e. ( TopOn ` CC ) )
35 13 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> D C_ CC )
36 eqid 
 |-  ( J |`t RR+ ) = ( J |`t RR+ )
37 2 36 cxpcn2 
 |-  ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( ( J |`t RR+ ) tX J ) Cn J )
38 37 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( ( J |`t RR+ ) tX J ) Cn J ) )
39 30 31 33 4 34 35 38 cnmpt2res 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( x e. RR+ , y e. D |-> ( x ^c y ) ) e. ( ( ( J |`t RR+ ) tX L ) Cn J ) )
40 elrege0 
 |-  ( u e. ( 0 [,) +oo ) <-> ( u e. RR /\ 0 <_ u ) )
41 40 simplbi 
 |-  ( u e. ( 0 [,) +oo ) -> u e. RR )
42 41 adantr 
 |-  ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> u e. RR )
43 42 adantr 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> u e. RR )
44 simpr 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> 0 < u )
45 43 44 elrpd 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> u e. RR+ )
46 simplr 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> v e. D )
47 45 46 opelxpd 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> <. u , v >. e. ( RR+ X. D ) )
48 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ D C_ CC ) -> ( J |`t D ) e. ( TopOn ` D ) )
49 21 13 48 mp2an 
 |-  ( J |`t D ) e. ( TopOn ` D )
50 4 49 eqeltri 
 |-  L e. ( TopOn ` D )
51 txtopon 
 |-  ( ( ( J |`t RR+ ) e. ( TopOn ` RR+ ) /\ L e. ( TopOn ` D ) ) -> ( ( J |`t RR+ ) tX L ) e. ( TopOn ` ( RR+ X. D ) ) )
52 29 50 51 mp2an 
 |-  ( ( J |`t RR+ ) tX L ) e. ( TopOn ` ( RR+ X. D ) )
53 52 toponunii 
 |-  ( RR+ X. D ) = U. ( ( J |`t RR+ ) tX L )
54 53 cncnpi 
 |-  ( ( ( x e. RR+ , y e. D |-> ( x ^c y ) ) e. ( ( ( J |`t RR+ ) tX L ) Cn J ) /\ <. u , v >. e. ( RR+ X. D ) ) -> ( x e. RR+ , y e. D |-> ( x ^c y ) ) e. ( ( ( ( J |`t RR+ ) tX L ) CnP J ) ` <. u , v >. ) )
55 39 47 54 syl2anc 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( x e. RR+ , y e. D |-> ( x ^c y ) ) e. ( ( ( ( J |`t RR+ ) tX L ) CnP J ) ` <. u , v >. ) )
56 ssid 
 |-  D C_ D
57 resmpo 
 |-  ( ( RR+ C_ ( 0 [,) +oo ) /\ D C_ D ) -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) |` ( RR+ X. D ) ) = ( x e. RR+ , y e. D |-> ( x ^c y ) ) )
58 26 56 57 mp2an 
 |-  ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) |` ( RR+ X. D ) ) = ( x e. RR+ , y e. D |-> ( x ^c y ) )
59 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( J |`t ( 0 [,) +oo ) ) e. ( TopOn ` ( 0 [,) +oo ) ) )
60 21 7 59 mp2an 
 |-  ( J |`t ( 0 [,) +oo ) ) e. ( TopOn ` ( 0 [,) +oo ) )
61 3 60 eqeltri 
 |-  K e. ( TopOn ` ( 0 [,) +oo ) )
62 ioorp 
 |-  ( 0 (,) +oo ) = RR+
63 iooretop 
 |-  ( 0 (,) +oo ) e. ( topGen ` ran (,) )
64 62 63 eqeltrri 
 |-  RR+ e. ( topGen ` ran (,) )
65 retop 
 |-  ( topGen ` ran (,) ) e. Top
66 ovex 
 |-  ( 0 [,) +oo ) e. _V
67 restopnb 
 |-  ( ( ( ( topGen ` ran (,) ) e. Top /\ ( 0 [,) +oo ) e. _V ) /\ ( RR+ e. ( topGen ` ran (,) ) /\ RR+ C_ ( 0 [,) +oo ) /\ RR+ C_ RR+ ) ) -> ( RR+ e. ( topGen ` ran (,) ) <-> RR+ e. ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) ) )
68 65 66 67 mpanl12 
 |-  ( ( RR+ e. ( topGen ` ran (,) ) /\ RR+ C_ ( 0 [,) +oo ) /\ RR+ C_ RR+ ) -> ( RR+ e. ( topGen ` ran (,) ) <-> RR+ e. ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) ) )
69 64 26 32 68 mp3an 
 |-  ( RR+ e. ( topGen ` ran (,) ) <-> RR+ e. ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) )
70 64 69 mpbi 
 |-  RR+ e. ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) )
71 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
72 2 71 rerest 
 |-  ( ( 0 [,) +oo ) C_ RR -> ( J |`t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) )
73 5 72 ax-mp 
 |-  ( J |`t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) )
74 3 73 eqtri 
 |-  K = ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) )
75 70 74 eleqtrri 
 |-  RR+ e. K
76 toponmax 
 |-  ( L e. ( TopOn ` D ) -> D e. L )
77 50 76 ax-mp 
 |-  D e. L
78 txrest 
 |-  ( ( ( K e. ( TopOn ` ( 0 [,) +oo ) ) /\ L e. ( TopOn ` D ) ) /\ ( RR+ e. K /\ D e. L ) ) -> ( ( K tX L ) |`t ( RR+ X. D ) ) = ( ( K |`t RR+ ) tX ( L |`t D ) ) )
79 61 50 75 77 78 mp4an 
 |-  ( ( K tX L ) |`t ( RR+ X. D ) ) = ( ( K |`t RR+ ) tX ( L |`t D ) )
80 3 oveq1i 
 |-  ( K |`t RR+ ) = ( ( J |`t ( 0 [,) +oo ) ) |`t RR+ )
81 restabs 
 |-  ( ( J e. ( TopOn ` CC ) /\ RR+ C_ ( 0 [,) +oo ) /\ ( 0 [,) +oo ) e. _V ) -> ( ( J |`t ( 0 [,) +oo ) ) |`t RR+ ) = ( J |`t RR+ ) )
82 21 26 66 81 mp3an 
 |-  ( ( J |`t ( 0 [,) +oo ) ) |`t RR+ ) = ( J |`t RR+ )
83 80 82 eqtri 
 |-  ( K |`t RR+ ) = ( J |`t RR+ )
84 50 toponunii 
 |-  D = U. L
85 84 restid 
 |-  ( L e. ( TopOn ` D ) -> ( L |`t D ) = L )
86 50 85 ax-mp 
 |-  ( L |`t D ) = L
87 83 86 oveq12i 
 |-  ( ( K |`t RR+ ) tX ( L |`t D ) ) = ( ( J |`t RR+ ) tX L )
88 79 87 eqtri 
 |-  ( ( K tX L ) |`t ( RR+ X. D ) ) = ( ( J |`t RR+ ) tX L )
89 88 oveq1i 
 |-  ( ( ( K tX L ) |`t ( RR+ X. D ) ) CnP J ) = ( ( ( J |`t RR+ ) tX L ) CnP J )
90 89 fveq1i 
 |-  ( ( ( ( K tX L ) |`t ( RR+ X. D ) ) CnP J ) ` <. u , v >. ) = ( ( ( ( J |`t RR+ ) tX L ) CnP J ) ` <. u , v >. )
91 55 58 90 3eltr4g 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) |` ( RR+ X. D ) ) e. ( ( ( ( K tX L ) |`t ( RR+ X. D ) ) CnP J ) ` <. u , v >. ) )
92 txtopon 
 |-  ( ( K e. ( TopOn ` ( 0 [,) +oo ) ) /\ L e. ( TopOn ` D ) ) -> ( K tX L ) e. ( TopOn ` ( ( 0 [,) +oo ) X. D ) ) )
93 61 50 92 mp2an 
 |-  ( K tX L ) e. ( TopOn ` ( ( 0 [,) +oo ) X. D ) )
94 93 topontopi 
 |-  ( K tX L ) e. Top
95 94 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( K tX L ) e. Top )
96 xpss1 
 |-  ( RR+ C_ ( 0 [,) +oo ) -> ( RR+ X. D ) C_ ( ( 0 [,) +oo ) X. D ) )
97 26 96 mp1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( RR+ X. D ) C_ ( ( 0 [,) +oo ) X. D ) )
98 txopn 
 |-  ( ( ( K e. ( TopOn ` ( 0 [,) +oo ) ) /\ L e. ( TopOn ` D ) ) /\ ( RR+ e. K /\ D e. L ) ) -> ( RR+ X. D ) e. ( K tX L ) )
99 61 50 75 77 98 mp4an 
 |-  ( RR+ X. D ) e. ( K tX L )
100 isopn3i 
 |-  ( ( ( K tX L ) e. Top /\ ( RR+ X. D ) e. ( K tX L ) ) -> ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) = ( RR+ X. D ) )
101 94 99 100 mp2an 
 |-  ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) = ( RR+ X. D )
102 47 101 eleqtrrdi 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> <. u , v >. e. ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) )
103 20 a1i 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC )
104 61 topontopi 
 |-  K e. Top
105 50 topontopi 
 |-  L e. Top
106 61 toponunii 
 |-  ( 0 [,) +oo ) = U. K
107 104 105 106 84 txunii 
 |-  ( ( 0 [,) +oo ) X. D ) = U. ( K tX L )
108 21 toponunii 
 |-  CC = U. J
109 107 108 cnprest 
 |-  ( ( ( ( K tX L ) e. Top /\ ( RR+ X. D ) C_ ( ( 0 [,) +oo ) X. D ) ) /\ ( <. u , v >. e. ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) /\ ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC ) ) -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) <-> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) |` ( RR+ X. D ) ) e. ( ( ( ( K tX L ) |`t ( RR+ X. D ) ) CnP J ) ` <. u , v >. ) ) )
110 95 97 102 103 109 syl22anc 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) <-> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) |` ( RR+ X. D ) ) e. ( ( ( ( K tX L ) |`t ( RR+ X. D ) ) CnP J ) ` <. u , v >. ) ) )
111 91 110 mpbird 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
112 20 a1i 
 |-  ( v e. D -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC )
113 eqid 
 |-  ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) = ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 )
114 eqid 
 |-  if ( ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) <_ ( e ^c ( 1 / ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) ) ) , ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) , ( e ^c ( 1 / ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) ) ) ) = if ( ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) <_ ( e ^c ( 1 / ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) ) ) , ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) , ( e ^c ( 1 / ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) ) ) )
115 1 2 3 4 113 114 cxpcn3lem 
 |-  ( ( v e. D /\ e e. RR+ ) -> E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < e ) )
116 115 ralrimiva 
 |-  ( v e. D -> A. e e. RR+ E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < e ) )
117 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
118 117 a1i 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> 0 e. ( 0 [,) +oo ) )
119 simprl 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> a e. ( 0 [,) +oo ) )
120 118 119 ovresd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) = ( 0 ( abs o. - ) a ) )
121 0cn 
 |-  0 e. CC
122 7 119 sselid 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> a e. CC )
123 eqid 
 |-  ( abs o. - ) = ( abs o. - )
124 123 cnmetdval 
 |-  ( ( 0 e. CC /\ a e. CC ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
125 121 122 124 sylancr 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
126 df-neg 
 |-  -u a = ( 0 - a )
127 126 fveq2i 
 |-  ( abs ` -u a ) = ( abs ` ( 0 - a ) )
128 122 absnegd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` -u a ) = ( abs ` a ) )
129 127 128 eqtr3id 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` ( 0 - a ) ) = ( abs ` a ) )
130 120 125 129 3eqtrd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) = ( abs ` a ) )
131 130 breq1d 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d <-> ( abs ` a ) < d ) )
132 simpl 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> v e. D )
133 simprr 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> b e. D )
134 132 133 ovresd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( ( abs o. - ) |` ( D X. D ) ) b ) = ( v ( abs o. - ) b ) )
135 13 132 sselid 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> v e. CC )
136 13 133 sselid 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> b e. CC )
137 123 cnmetdval 
 |-  ( ( v e. CC /\ b e. CC ) -> ( v ( abs o. - ) b ) = ( abs ` ( v - b ) ) )
138 135 136 137 syl2anc 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( abs o. - ) b ) = ( abs ` ( v - b ) ) )
139 134 138 eqtrd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( ( abs o. - ) |` ( D X. D ) ) b ) = ( abs ` ( v - b ) ) )
140 139 breq1d 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d <-> ( abs ` ( v - b ) ) < d ) )
141 131 140 anbi12d 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) <-> ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) ) )
142 oveq12 
 |-  ( ( x = 0 /\ y = v ) -> ( x ^c y ) = ( 0 ^c v ) )
143 ovex 
 |-  ( 0 ^c v ) e. _V
144 142 18 143 ovmpoa 
 |-  ( ( 0 e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) = ( 0 ^c v ) )
145 117 132 144 sylancr 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) = ( 0 ^c v ) )
146 1 eleq2i 
 |-  ( v e. D <-> v e. ( `' Re " RR+ ) )
147 ffn 
 |-  ( Re : CC --> RR -> Re Fn CC )
148 elpreima 
 |-  ( Re Fn CC -> ( v e. ( `' Re " RR+ ) <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) ) )
149 10 147 148 mp2b 
 |-  ( v e. ( `' Re " RR+ ) <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) )
150 146 149 bitri 
 |-  ( v e. D <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) )
151 150 simplbi 
 |-  ( v e. D -> v e. CC )
152 150 simprbi 
 |-  ( v e. D -> ( Re ` v ) e. RR+ )
153 152 rpne0d 
 |-  ( v e. D -> ( Re ` v ) =/= 0 )
154 fveq2 
 |-  ( v = 0 -> ( Re ` v ) = ( Re ` 0 ) )
155 re0 
 |-  ( Re ` 0 ) = 0
156 154 155 eqtrdi 
 |-  ( v = 0 -> ( Re ` v ) = 0 )
157 156 necon3i 
 |-  ( ( Re ` v ) =/= 0 -> v =/= 0 )
158 153 157 syl 
 |-  ( v e. D -> v =/= 0 )
159 151 158 0cxpd 
 |-  ( v e. D -> ( 0 ^c v ) = 0 )
160 159 adantr 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ^c v ) = 0 )
161 145 160 eqtrd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) = 0 )
162 oveq12 
 |-  ( ( x = a /\ y = b ) -> ( x ^c y ) = ( a ^c b ) )
163 ovex 
 |-  ( a ^c b ) e. _V
164 162 18 163 ovmpoa 
 |-  ( ( a e. ( 0 [,) +oo ) /\ b e. D ) -> ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) = ( a ^c b ) )
165 164 adantl 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) = ( a ^c b ) )
166 161 165 oveq12d 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) = ( 0 ( abs o. - ) ( a ^c b ) ) )
167 122 136 cxpcld 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( a ^c b ) e. CC )
168 123 cnmetdval 
 |-  ( ( 0 e. CC /\ ( a ^c b ) e. CC ) -> ( 0 ( abs o. - ) ( a ^c b ) ) = ( abs ` ( 0 - ( a ^c b ) ) ) )
169 121 167 168 sylancr 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( abs o. - ) ( a ^c b ) ) = ( abs ` ( 0 - ( a ^c b ) ) ) )
170 df-neg 
 |-  -u ( a ^c b ) = ( 0 - ( a ^c b ) )
171 170 fveq2i 
 |-  ( abs ` -u ( a ^c b ) ) = ( abs ` ( 0 - ( a ^c b ) ) )
172 167 absnegd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` -u ( a ^c b ) ) = ( abs ` ( a ^c b ) ) )
173 171 172 eqtr3id 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` ( 0 - ( a ^c b ) ) ) = ( abs ` ( a ^c b ) ) )
174 166 169 173 3eqtrd 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) = ( abs ` ( a ^c b ) ) )
175 174 breq1d 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e <-> ( abs ` ( a ^c b ) ) < e ) )
176 141 175 imbi12d 
 |-  ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) <-> ( ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < e ) ) )
177 176 2ralbidva 
 |-  ( v e. D -> ( A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) <-> A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < e ) ) )
178 177 rexbidv 
 |-  ( v e. D -> ( E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) <-> E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < e ) ) )
179 178 ralbidv 
 |-  ( v e. D -> ( A. e e. RR+ E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) <-> A. e e. RR+ E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( v - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < e ) ) )
180 116 179 mpbird 
 |-  ( v e. D -> A. e e. RR+ E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) )
181 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
182 181 a1i 
 |-  ( v e. D -> ( abs o. - ) e. ( *Met ` CC ) )
183 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( *Met ` ( 0 [,) +oo ) ) )
184 182 7 183 sylancl 
 |-  ( v e. D -> ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( *Met ` ( 0 [,) +oo ) ) )
185 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ D C_ CC ) -> ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) )
186 182 13 185 sylancl 
 |-  ( v e. D -> ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) )
187 117 a1i 
 |-  ( v e. D -> 0 e. ( 0 [,) +oo ) )
188 id 
 |-  ( v e. D -> v e. D )
189 eqid 
 |-  ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) = ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) )
190 2 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
191 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
192 189 190 191 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( J |`t ( 0 [,) +oo ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) )
193 181 7 192 mp2an 
 |-  ( J |`t ( 0 [,) +oo ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
194 3 193 eqtri 
 |-  K = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
195 eqid 
 |-  ( ( abs o. - ) |` ( D X. D ) ) = ( ( abs o. - ) |` ( D X. D ) )
196 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
197 195 190 196 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ D C_ CC ) -> ( J |`t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) )
198 181 13 197 mp2an 
 |-  ( J |`t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
199 4 198 eqtri 
 |-  L = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
200 194 199 190 txmetcnp 
 |-  ( ( ( ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( *Met ` ( 0 [,) +oo ) ) /\ ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) /\ ( abs o. - ) e. ( *Met ` CC ) ) /\ ( 0 e. ( 0 [,) +oo ) /\ v e. D ) ) -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) <-> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC /\ A. e e. RR+ E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) ) ) )
201 184 186 182 187 188 200 syl32anc 
 |-  ( v e. D -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) <-> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC /\ A. e e. RR+ E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d /\ ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d ) -> ( ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) ( abs o. - ) ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) ) < e ) ) ) )
202 112 180 201 mpbir2and 
 |-  ( v e. D -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) )
203 202 ad2antlr 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) )
204 simpr 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> 0 = u )
205 204 opeq1d 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> <. 0 , v >. = <. u , v >. )
206 205 fveq2d 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) = ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
207 203 206 eleqtrd 
 |-  ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
208 40 simprbi 
 |-  ( u e. ( 0 [,) +oo ) -> 0 <_ u )
209 208 adantr 
 |-  ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> 0 <_ u )
210 0re 
 |-  0 e. RR
211 leloe 
 |-  ( ( 0 e. RR /\ u e. RR ) -> ( 0 <_ u <-> ( 0 < u \/ 0 = u ) ) )
212 210 42 211 sylancr 
 |-  ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 <_ u <-> ( 0 < u \/ 0 = u ) ) )
213 209 212 mpbid 
 |-  ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 < u \/ 0 = u ) )
214 111 207 213 mpjaodan 
 |-  ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
215 214 rgen2 
 |-  A. u e. ( 0 [,) +oo ) A. v e. D ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. )
216 fveq2 
 |-  ( z = <. u , v >. -> ( ( ( K tX L ) CnP J ) ` z ) = ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
217 216 eleq2d 
 |-  ( z = <. u , v >. -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` z ) <-> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) ) )
218 217 ralxp 
 |-  ( A. z e. ( ( 0 [,) +oo ) X. D ) ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` z ) <-> A. u e. ( 0 [,) +oo ) A. v e. D ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
219 215 218 mpbir 
 |-  A. z e. ( ( 0 [,) +oo ) X. D ) ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` z )
220 cncnp 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( ( 0 [,) +oo ) X. D ) ) /\ J e. ( TopOn ` CC ) ) -> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J ) <-> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC /\ A. z e. ( ( 0 [,) +oo ) X. D ) ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` z ) ) ) )
221 93 21 220 mp2an 
 |-  ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J ) <-> ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC /\ A. z e. ( ( 0 [,) +oo ) X. D ) ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` z ) ) )
222 20 219 221 mpbir2an 
 |-  ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J )