Theorem cxpcn3 22318

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.)

Hypotheses

Ref	Expression
cxpcn3.d	|- D = ( `' Re " RR+ )
cxpcn3.j	|- J = ( TopOpen ` ℂfld )
cxpcn3.k	|- K = ( J ↾t ( 0 [,) +oo ) )
cxpcn3.l	|- L = ( J ↾t D )

Assertion

Ref	Expression
cxpcn3	|- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J )

Distinct variable groups:   x, y, J   x, D, y

Allowed substitution hints:   K( x, y)   L( x, y)

Proof of Theorem cxpcn3

Dummy variables a b d e u v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0re 9496	. . . . . . . 8 |- 0 e. RR
2		pnfxr 11202	. . . . . . . 8 |- +oo e. RR*
3		icossre 11486	. . . . . . . 8 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
4	1, 2, 3	mp2an 672	. . . . . . 7 |- ( 0 [,) +oo ) C_ RR
5		ax-resscn 9449	. . . . . . 7 |- RR C_ CC
6	4, 5	sstri 3472	. . . . . 6 |- ( 0 [,) +oo ) C_ CC
7	6	sseli 3459	. . . . 5 |- ( x e. ( 0 [,) +oo ) -> x e. CC )
8		cxpcn3.d	. . . . . . 7 |- D = ( `' Re " RR+ )
9		cnvimass 5296	. . . . . . . 8 |- ( `' Re " RR+ ) C_ dom Re
10		ref 12718	. . . . . . . . 9 |- Re : CC --> RR
11	10	fdmi 5671	. . . . . . . 8 |- dom Re = CC
12	9, 11	sseqtri 3495	. . . . . . 7 |- ( `' Re " RR+ ) C_ CC
13	8, 12	eqsstri 3493	. . . . . 6 |- D C_ CC
14	13	sseli 3459	. . . . 5 |- ( y e. D -> y e. CC )
15		cxpcl 22251	. . . . 5 |- ( ( x e. CC /\ y e. CC ) -> ( x ^c y ) e. CC )
16	7, 14, 15	syl2an 477	. . . 4 |- ( ( x e. ( 0 [,) +oo ) /\ y e. D ) -> ( x ^c y ) e. CC )
17	16	rgen2 2916	. . 3 |- A. x e. ( 0 [,) +oo ) A. y e. D ( x ^c y ) e. CC
18		eqid 2454	. . . 4 |- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) = ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) )
19	18	fmpt2 6750	. . 3 |- ( 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 208	. 2 |- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC
21		cxpcn3.j	. . . . . . . . . . . . 13 |- J = ( TopOpen ` ℂfld )
22	21	cnfldtopon 20493	. . . . . . . . . . . 12 |- J e. (TopOn ` CC )
23		rpre 11107	. . . . . . . . . . . . . . 15 |- ( x e. RR+ -> x e. RR )
24		rpge0 11113	. . . . . . . . . . . . . . 15 |- ( x e. RR+ -> 0 <_ x )
25		elrege0 11508	. . . . . . . . . . . . . . 15 |- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
26	23, 24, 25	sylanbrc 664	. . . . . . . . . . . . . 14 |- ( x e. RR+ -> x e. ( 0 [,) +oo ) )
27	26	ssriv 3467	. . . . . . . . . . . . 13 |- RR+ C_ ( 0 [,) +oo )
28	27, 6	sstri 3472	. . . . . . . . . . . 12 |- RR+ C_ CC
29		resttopon 18896	. . . . . . . . . . . 12 |- ( ( J e. (TopOn ` CC ) /\ RR+ C_ CC ) -> ( J ↾t RR+ ) e. (TopOn ` RR+ ) )
30	22, 28, 29	mp2an 672	. . . . . . . . . . 11 |- ( J ↾t RR+ ) e. (TopOn ` RR+ )
31	30	toponunii 18668	. . . . . . . . . . . 12 |- RR+ = U. ( J ↾t RR+ )
32	31	restid 14490	. . . . . . . . . . 11 |- ( ( J ↾t RR+ ) e. (TopOn ` RR+ ) -> ( ( J ↾t RR+ ) ↾t RR+ ) = ( J ↾t RR+ ) )
33	30, 32	ax-mp 5	. . . . . . . . . 10 |- ( ( J ↾t RR+ ) ↾t RR+ ) = ( J ↾t RR+ )
34	33	eqcomi 2467	. . . . . . . . 9 |- ( J ↾t RR+ ) = ( ( J ↾t RR+ ) ↾t RR+ )
35	30	a1i 11	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( J ↾t RR+ ) e. (TopOn ` RR+ ) )
36		ssid 3482	. . . . . . . . . 10 |- RR+ C_ RR+
37	36	a1i 11	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> RR+ C_ RR+ )
38		cxpcn3.l	. . . . . . . . 9 |- L = ( J ↾t D )
39	22	a1i 11	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> J e. (TopOn ` CC ) )
40	13	a1i 11	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> D C_ CC )
41		eqid 2454	. . . . . . . . . . 11 |- ( J ↾t RR+ ) = ( J ↾t RR+ )
42	21, 41	cxpcn2 22316	. . . . . . . . . 10 |- ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( ( J ↾t RR+ ) tX J ) Cn J )
43	42	a1i 11	. . . . . . . . 9 |- ( ( ( 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 ) )
44	34, 35, 37, 38, 39, 40, 43	cnmpt2res 19381	. . . . . . . 8 |- ( ( ( 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 ) )
45		elrege0 11508	. . . . . . . . . . . . 13 |- ( u e. ( 0 [,) +oo ) <-> ( u e. RR /\ 0 <_ u ) )
46	45	simplbi 460	. . . . . . . . . . . 12 |- ( u e. ( 0 [,) +oo ) -> u e. RR )
47	46	adantr 465	. . . . . . . . . . 11 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> u e. RR )
48	47	adantr 465	. . . . . . . . . 10 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> u e. RR )
49		simpr 461	. . . . . . . . . 10 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> 0 < u )
50	48, 49	elrpd 11135	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> u e. RR+ )
51		simplr 754	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> v e. D )
52		opelxp 4976	. . . . . . . . 9 |- ( <. u , v >. e. ( RR+ X. D ) <-> ( u e. RR+ /\ v e. D ) )
53	50, 51, 52	sylanbrc 664	. . . . . . . 8 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> <. u , v >. e. ( RR+ X. D ) )
54		resttopon 18896	. . . . . . . . . . . . 13 |- ( ( J e. (TopOn ` CC ) /\ D C_ CC ) -> ( J ↾t D ) e. (TopOn ` D ) )
55	22, 13, 54	mp2an 672	. . . . . . . . . . . 12 |- ( J ↾t D ) e. (TopOn ` D )
56	38, 55	eqeltri 2538	. . . . . . . . . . 11 |- L e. (TopOn ` D )
57		txtopon 19295	. . . . . . . . . . 11 |- ( ( ( J ↾t RR+ ) e. (TopOn ` RR+ ) /\ L e. (TopOn ` D ) ) -> ( ( J ↾t RR+ ) tX L ) e. (TopOn ` ( RR+ X. D ) ) )
58	30, 56, 57	mp2an 672	. . . . . . . . . 10 |- ( ( J ↾t RR+ ) tX L ) e. (TopOn ` ( RR+ X. D ) )
59	58	toponunii 18668	. . . . . . . . 9 |- ( RR+ X. D ) = U. ( ( J ↾t RR+ ) tX L )
60	59	cncnpi 19013	. . . . . . . 8 |- ( ( ( 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 >. ) )
61	44, 53, 60	syl2anc 661	. . . . . . 7 |- ( ( ( 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 >. ) )
62		ssid 3482	. . . . . . . 8 |- D C_ D
63		resmpt2 6297	. . . . . . . 8 |- ( ( 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 ) ) )
64	27, 62, 63	mp2an 672	. . . . . . 7 |- ( ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) |` ( RR+ X. D ) ) = ( x e. RR+ , y e. D |-> ( x ^c y ) )
65		cxpcn3.k	. . . . . . . . . . . 12 |- K = ( J ↾t ( 0 [,) +oo ) )
66		resttopon 18896	. . . . . . . . . . . . 13 |- ( ( J e. (TopOn ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( J ↾t ( 0 [,) +oo ) ) e. (TopOn ` ( 0 [,) +oo ) ) )
67	22, 6, 66	mp2an 672	. . . . . . . . . . . 12 |- ( J ↾t ( 0 [,) +oo ) ) e. (TopOn ` ( 0 [,) +oo ) )
68	65, 67	eqeltri 2538	. . . . . . . . . . 11 |- K e. (TopOn ` ( 0 [,) +oo ) )
69		ioorp 11483	. . . . . . . . . . . . . 14 |- ( 0 (,) +oo ) = RR+
70		iooretop 20476	. . . . . . . . . . . . . 14 |- ( 0 (,) +oo ) e. ( topGen ` ran (,) )
71	69, 70	eqeltrri 2539	. . . . . . . . . . . . 13 |- RR+ e. ( topGen ` ran (,) )
72		retop 20471	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) e. Top
73		ovex 6224	. . . . . . . . . . . . . . 15 |- ( 0 [,) +oo ) e. _V
74		restopnb 18910	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) ) )
75	72, 73, 74	mpanl12 682	. . . . . . . . . . . . . 14 |- ( ( RR+ e. ( topGen ` ran (,) ) /\ RR+ C_ ( 0 [,) +oo ) /\ RR+ C_ RR+ ) -> ( RR+ e. ( topGen ` ran (,) ) <-> RR+ e. ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) ) ) )
76	71, 27, 36, 75	mp3an 1315	. . . . . . . . . . . . 13 |- ( RR+ e. ( topGen ` ran (,) ) <-> RR+ e. ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) ) )
77	71, 76	mpbi 208	. . . . . . . . . . . 12 |- RR+ e. ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) )
78		eqid 2454	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
79	21, 78	rerest 20512	. . . . . . . . . . . . . 14 |- ( ( 0 [,) +oo ) C_ RR -> ( J ↾t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) ) )
80	4, 79	ax-mp 5	. . . . . . . . . . . . 13 |- ( J ↾t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) )
81	65, 80	eqtri 2483	. . . . . . . . . . . 12 |- K = ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) )
82	77, 81	eleqtrri 2541	. . . . . . . . . . 11 |- RR+ e. K
83		toponmax 18664	. . . . . . . . . . . 12 |- ( L e. (TopOn ` D ) -> D e. L )
84	56, 83	ax-mp 5	. . . . . . . . . . 11 |- D e. L
85		txrest 19335	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
86	68, 56, 82, 84, 85	mp4an 673	. . . . . . . . . 10 |- ( ( K tX L ) ↾t ( RR+ X. D ) ) = ( ( K ↾t RR+ ) tX ( L ↾t D ) )
87	65	oveq1i 6209	. . . . . . . . . . . 12 |- ( K ↾t RR+ ) = ( ( J ↾t ( 0 [,) +oo ) ) ↾t RR+ )
88		restabs 18900	. . . . . . . . . . . . 13 |- ( ( J e. (TopOn ` CC ) /\ RR+ C_ ( 0 [,) +oo ) /\ ( 0 [,) +oo ) e. _V ) -> ( ( J ↾t ( 0 [,) +oo ) ) ↾t RR+ ) = ( J ↾t RR+ ) )
89	22, 27, 73, 88	mp3an 1315	. . . . . . . . . . . 12 |- ( ( J ↾t ( 0 [,) +oo ) ) ↾t RR+ ) = ( J ↾t RR+ )
90	87, 89	eqtri 2483	. . . . . . . . . . 11 |- ( K ↾t RR+ ) = ( J ↾t RR+ )
91	56	toponunii 18668	. . . . . . . . . . . . 13 |- D = U. L
92	91	restid 14490	. . . . . . . . . . . 12 |- ( L e. (TopOn ` D ) -> ( L ↾t D ) = L )
93	56, 92	ax-mp 5	. . . . . . . . . . 11 |- ( L ↾t D ) = L
94	90, 93	oveq12i 6211	. . . . . . . . . 10 |- ( ( K ↾t RR+ ) tX ( L ↾t D ) ) = ( ( J ↾t RR+ ) tX L )
95	86, 94	eqtri 2483	. . . . . . . . 9 |- ( ( K tX L ) ↾t ( RR+ X. D ) ) = ( ( J ↾t RR+ ) tX L )
96	95	oveq1i 6209	. . . . . . . 8 |- ( ( ( K tX L ) ↾t ( RR+ X. D ) ) CnP J ) = ( ( ( J ↾t RR+ ) tX L ) CnP J )
97	96	fveq1i 5799	. . . . . . 7 |- ( ( ( ( K tX L ) ↾t ( RR+ X. D ) ) CnP J ) ` <. u , v >. ) = ( ( ( ( J ↾t RR+ ) tX L ) CnP J ) ` <. u , v >. )
98	61, 64, 97	3eltr4g 2560	. . . . . 6 |- ( ( ( 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 >. ) )
99		txtopon 19295	. . . . . . . . . 10 |- ( ( K e. (TopOn ` ( 0 [,) +oo ) ) /\ L e. (TopOn ` D ) ) -> ( K tX L ) e. (TopOn ` ( ( 0 [,) +oo ) X. D ) ) )
100	68, 56, 99	mp2an 672	. . . . . . . . 9 |- ( K tX L ) e. (TopOn ` ( ( 0 [,) +oo ) X. D ) )
101	100	topontopi 18667	. . . . . . . 8 |- ( K tX L ) e. Top
102	101	a1i 11	. . . . . . 7 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( K tX L ) e. Top )
103		xpss1 5055	. . . . . . . 8 |- ( RR+ C_ ( 0 [,) +oo ) -> ( RR+ X. D ) C_ ( ( 0 [,) +oo ) X. D ) )
104	27, 103	mp1i 12	. . . . . . 7 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( RR+ X. D ) C_ ( ( 0 [,) +oo ) X. D ) )
105		txopn 19306	. . . . . . . . . 10 |- ( ( ( K e. (TopOn ` ( 0 [,) +oo ) ) /\ L e. (TopOn ` D ) ) /\ ( RR+ e. K /\ D e. L ) ) -> ( RR+ X. D ) e. ( K tX L ) )
106	68, 56, 82, 84, 105	mp4an 673	. . . . . . . . 9 |- ( RR+ X. D ) e. ( K tX L )
107		isopn3i 18817	. . . . . . . . 9 |- ( ( ( K tX L ) e. Top /\ ( RR+ X. D ) e. ( K tX L ) ) -> ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) = ( RR+ X. D ) )
108	101, 106, 107	mp2an 672	. . . . . . . 8 |- ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) = ( RR+ X. D )
109	53, 108	syl6eleqr 2553	. . . . . . 7 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> <. u , v >. e. ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) )
110	20	a1i 11	. . . . . . 7 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC )
111	68	topontopi 18667	. . . . . . . . 9 |- K e. Top
112	56	topontopi 18667	. . . . . . . . 9 |- L e. Top
113	68	toponunii 18668	. . . . . . . . 9 |- ( 0 [,) +oo ) = U. K
114	111, 112, 113, 91	txunii 19297	. . . . . . . 8 |- ( ( 0 [,) +oo ) X. D ) = U. ( K tX L )
115	22	toponunii 18668	. . . . . . . 8 |- CC = U. J
116	114, 115	cnprest 19024	. . . . . . 7 |- ( ( ( ( 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 >. ) ) )
117	102, 104, 109, 110, 116	syl22anc 1220	. . . . . 6 |- ( ( ( 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 >. ) ) )
118	98, 117	mpbird 232	. . . . 5 |- ( ( ( 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 >. ) )
119	20	a1i 11	. . . . . . . 8 |- ( v e. D -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) : ( ( 0 [,) +oo ) X. D ) --> CC )
120		eqid 2454	. . . . . . . . . . 11 |- ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) = ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 )
121		eqid 2454	. . . . . . . . . . 11 |- 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 ) ) ) )
122	8, 21, 65, 38, 120, 121	cxpcn3lem 22317	. . . . . . . . . 10 |- ( ( 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 ) )
123	122	ralrimiva 2829	. . . . . . . . 9 |- ( 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 ) )
124		0e0icopnf 11511	. . . . . . . . . . . . . . . . . 18 |- 0 e. ( 0 [,) +oo )
125	124	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> 0 e. ( 0 [,) +oo ) )
126		simprl 755	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> a e. ( 0 [,) +oo ) )
127	125, 126	ovresd 6340	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) = ( 0 ( abs o. - ) a ) )
128		0cn 9488	. . . . . . . . . . . . . . . . 17 |- 0 e. CC
129	6, 126	sseldi 3461	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> a e. CC )
130		eqid 2454	. . . . . . . . . . . . . . . . . 18 |- ( abs o. - ) = ( abs o. - )
131	130	cnmetdval 20481	. . . . . . . . . . . . . . . . 17 |- ( ( 0 e. CC /\ a e. CC ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
132	128, 129, 131	sylancr 663	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
133		df-neg 9708	. . . . . . . . . . . . . . . . . 18 |- -u a = ( 0 - a )
134	133	fveq2i 5801	. . . . . . . . . . . . . . . . 17 |- ( abs ` -u a ) = ( abs ` ( 0 - a ) )
135	129	absnegd 13052	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` -u a ) = ( abs ` a ) )
136	134, 135	syl5eqr 2509	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` ( 0 - a ) ) = ( abs ` a ) )
137	127, 132, 136	3eqtrd 2499	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) = ( abs ` a ) )
138	137	breq1d 4409	. . . . . . . . . . . . . 14 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d <-> ( abs ` a ) < d ) )
139		simpl 457	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> v e. D )
140		simprr 756	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> b e. D )
141	139, 140	ovresd 6340	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( ( abs o. - ) |` ( D X. D ) ) b ) = ( v ( abs o. - ) b ) )
142	13, 139	sseldi 3461	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> v e. CC )
143	13, 140	sseldi 3461	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> b e. CC )
144	130	cnmetdval 20481	. . . . . . . . . . . . . . . . 17 |- ( ( v e. CC /\ b e. CC ) -> ( v ( abs o. - ) b ) = ( abs ` ( v - b ) ) )
145	142, 143, 144	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( abs o. - ) b ) = ( abs ` ( v - b ) ) )
146	141, 145	eqtrd 2495	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( ( abs o. - ) |` ( D X. D ) ) b ) = ( abs ` ( v - b ) ) )
147	146	breq1d 4409	. . . . . . . . . . . . . 14 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d <-> ( abs ` ( v - b ) ) < d ) )
148	138, 147	anbi12d 710	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
149		oveq12 6208	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = 0 /\ y = v ) -> ( x ^c y ) = ( 0 ^c v ) )
150		ovex 6224	. . . . . . . . . . . . . . . . . . 19 |- ( 0 ^c v ) e. _V
151	149, 18, 150	ovmpt2a 6330	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) = ( 0 ^c v ) )
152	124, 139, 151	sylancr 663	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) )
153	8	eleq2i 2532	. . . . . . . . . . . . . . . . . . . . 21 |- ( v e. D <-> v e. ( `' Re " RR+ ) )
154		ffn 5666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Re : CC --> RR -> Re Fn CC )
155		elpreima 5931	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Re Fn CC -> ( v e. ( `' Re " RR+ ) <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) ) )
156	10, 154, 155	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 |- ( v e. ( `' Re " RR+ ) <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) )
157	153, 156	bitri 249	. . . . . . . . . . . . . . . . . . . 20 |- ( v e. D <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) )
158	157	simplbi 460	. . . . . . . . . . . . . . . . . . 19 |- ( v e. D -> v e. CC )
159	157	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( v e. D -> ( Re ` v ) e. RR+ )
160	159	rpne0d 11142	. . . . . . . . . . . . . . . . . . . 20 |- ( v e. D -> ( Re ` v ) =/= 0 )
161		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . 22 |- ( v = 0 -> ( Re ` v ) = ( Re ` 0 ) )
162		re0 12758	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Re ` 0 ) = 0
163	161, 162	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . 21 |- ( v = 0 -> ( Re ` v ) = 0 )
164	163	necon3i 2691	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Re ` v ) =/= 0 -> v =/= 0 )
165	160, 164	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( v e. D -> v =/= 0 )
166	158, 165	0cxpd 22287	. . . . . . . . . . . . . . . . . 18 |- ( v e. D -> ( 0 ^c v ) = 0 )
167	166	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ^c v ) = 0 )
168	152, 167	eqtrd 2495	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) v ) = 0 )
169		oveq12 6208	. . . . . . . . . . . . . . . . . 18 |- ( ( x = a /\ y = b ) -> ( x ^c y ) = ( a ^c b ) )
170		ovex 6224	. . . . . . . . . . . . . . . . . 18 |- ( a ^c b ) e. _V
171	169, 18, 170	ovmpt2a 6330	. . . . . . . . . . . . . . . . 17 |- ( ( a e. ( 0 [,) +oo ) /\ b e. D ) -> ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) b ) = ( a ^c b ) )
172	171	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) )
173	168, 172	oveq12d 6217	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) )
174	129, 143	cxpcld 22285	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( a ^c b ) e. CC )
175	130	cnmetdval 20481	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. CC /\ ( a ^c b ) e. CC ) -> ( 0 ( abs o. - ) ( a ^c b ) ) = ( abs ` ( 0 - ( a ^c b ) ) ) )
176	128, 174, 175	sylancr 663	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( abs o. - ) ( a ^c b ) ) = ( abs ` ( 0 - ( a ^c b ) ) ) )
177		df-neg 9708	. . . . . . . . . . . . . . . . 17 |- -u ( a ^c b ) = ( 0 - ( a ^c b ) )
178	177	fveq2i 5801	. . . . . . . . . . . . . . . 16 |- ( abs ` -u ( a ^c b ) ) = ( abs ` ( 0 - ( a ^c b ) ) )
179	174	absnegd 13052	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` -u ( a ^c b ) ) = ( abs ` ( a ^c b ) ) )
180	178, 179	syl5eqr 2509	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` ( 0 - ( a ^c b ) ) ) = ( abs ` ( a ^c b ) ) )
181	173, 176, 180	3eqtrd 2499	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
182	181	breq1d 4409	. . . . . . . . . . . . 13 |- ( ( 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 ) )
183	148, 182	imbi12d 320	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
184	183	2ralbidva 2849	. . . . . . . . . . 11 |- ( 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 ) ) )
185	184	rexbidv 2864	. . . . . . . . . 10 |- ( 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 ) ) )
186	185	ralbidv 2845	. . . . . . . . 9 |- ( 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 ) ) )
187	123, 186	mpbird 232	. . . . . . . 8 |- ( 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 ) )
188		cnxmet 20483	. . . . . . . . . . 11 |- ( abs o. - ) e. ( *Met ` CC )
189	188	a1i 11	. . . . . . . . . 10 |- ( v e. D -> ( abs o. - ) e. ( *Met ` CC ) )
190		xmetres2 20067	. . . . . . . . . 10 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( *Met ` ( 0 [,) +oo ) ) )
191	189, 6, 190	sylancl 662	. . . . . . . . 9 |- ( v e. D -> ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( *Met ` ( 0 [,) +oo ) ) )
192		xmetres2 20067	. . . . . . . . . 10 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ D C_ CC ) -> ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) )
193	189, 13, 192	sylancl 662	. . . . . . . . 9 |- ( v e. D -> ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) )
194	124	a1i 11	. . . . . . . . 9 |- ( v e. D -> 0 e. ( 0 [,) +oo ) )
195		id 22	. . . . . . . . 9 |- ( v e. D -> v e. D )
196		eqid 2454	. . . . . . . . . . . . 13 |- ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) = ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) )
197	21	cnfldtopn 20492	. . . . . . . . . . . . 13 |- J = ( MetOpen ` ( abs o. - ) )
198		eqid 2454	. . . . . . . . . . . . 13 |- ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
199	196, 197, 198	metrest 20230	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( J ↾t ( 0 [,) +oo ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) )
200	188, 6, 199	mp2an 672	. . . . . . . . . . 11 |- ( J ↾t ( 0 [,) +oo ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
201	65, 200	eqtri 2483	. . . . . . . . . 10 |- K = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
202		eqid 2454	. . . . . . . . . . . . 13 |- ( ( abs o. - ) |` ( D X. D ) ) = ( ( abs o. - ) |` ( D X. D ) )
203		eqid 2454	. . . . . . . . . . . . 13 |- ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
204	202, 197, 203	metrest 20230	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ D C_ CC ) -> ( J ↾t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) )
205	188, 13, 204	mp2an 672	. . . . . . . . . . 11 |- ( J ↾t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
206	38, 205	eqtri 2483	. . . . . . . . . 10 |- L = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
207	201, 206, 197	txmetcnp 20253	. . . . . . . . 9 |- ( ( ( ( ( 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 ) ) ) )
208	191, 193, 189, 194, 195, 207	syl32anc 1227	. . . . . . . 8 |- ( 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 ) ) ) )
209	119, 187, 208	mpbir2and 913	. . . . . . 7 |- ( v e. D -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) )
210	209	ad2antlr 726	. . . . . 6 |- ( ( ( 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 >. ) )
211		simpr 461	. . . . . . . 8 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> 0 = u )
212	211	opeq1d 4172	. . . . . . 7 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> <. 0 , v >. = <. u , v >. )
213	212	fveq2d 5802	. . . . . 6 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) = ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
214	210, 213	eleqtrd 2544	. . . . 5 |- ( ( ( 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 >. ) )
215	45	simprbi 464	. . . . . . 7 |- ( u e. ( 0 [,) +oo ) -> 0 <_ u )
216	215	adantr 465	. . . . . 6 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> 0 <_ u )
217		leloe 9571	. . . . . . 7 |- ( ( 0 e. RR /\ u e. RR ) -> ( 0 <_ u <-> ( 0 < u \/ 0 = u ) ) )
218	1, 47, 217	sylancr 663	. . . . . 6 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 <_ u <-> ( 0 < u \/ 0 = u ) ) )
219	216, 218	mpbid 210	. . . . 5 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 < u \/ 0 = u ) )
220	118, 214, 219	mpjaodan 784	. . . 4 |- ( ( 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 >. ) )
221	220	rgen2 2916	. . 3 |- 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 >. )
222		fveq2 5798	. . . . 5 |- ( z = <. u , v >. -> ( ( ( K tX L ) CnP J ) ` z ) = ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
223	222	eleq2d 2524	. . . 4 |- ( 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 >. ) ) )
224	223	ralxp 5088	. . 3 |- ( 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 >. ) )
225	221, 224	mpbir 209	. 2 |- A. z e. ( ( 0 [,) +oo ) X. D ) ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( ( K tX L ) CnP J ) ` z )
226		cncnp 19015	. . 3 |- ( ( ( 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 ) ) ) )
227	100, 22, 226	mp2an 672	. 2 |- ( ( 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 ) ) )
228	20, 225, 227	mpbir2an 911	1 |- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   =/= wne 2647   A.wral 2798   E.wrex 2799   _Vcvv 3076   C_ wss 3435   ifcif 3898   <.cop 3990   class class class wbr 4399   X. cxp 4945   `'ccnv 4946   dom cdm 4947   ran crn 4948   |` cres 4949   "cima 4950   o. ccom 4951   Fn wfn 5520   -->wf 5521   ` cfv 5525  (class class class)co 6199   |-> cmpt2 6201   CCcc 9390   RRcr 9391   0cc0 9392   1c1 9393   +oocpnf 9525   RR*cxr 9527   < clt 9528   <_ cle 9529   - cmin 9705   -ucneg 9706   / cdiv 10103   2c2 10481   RR+crp 11101   (,)cioo 11410   [,)cico 11412   Recre 12703   abscabs 12840   ↾_t crest 14477   TopOpenctopn 14478   topGenctg 14494   *Metcxmt 17925   MetOpencmopn 17930  ℂ_fldccnfld 17942   Topctop 18629  TopOnctopon 18630   intcnt 18752   Cn ccn 18959   CnP ccnp 18960   tX ctx 19264   ^c ccxp 22139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-inf2 7957  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469  ax-pre-sup 9470  ax-addf 9471  ax-mulf 9472

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-iin 4281  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-se 4787  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-of 6429  df-om 6586  df-1st 6686  df-2nd 6687  df-supp 6800  df-recs 6941  df-rdg 6975  df-1o 7029  df-2o 7030  df-oadd 7033  df-er 7210  df-map 7325  df-pm 7326  df-ixp 7373  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-fsupp 7731  df-fi 7771  df-sup 7801  df-oi 7834  df-card 8219  df-cda 8447  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-div 10104  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-5 10493  df-6 10494  df-7 10495  df-8 10496  df-9 10497  df-10 10498  df-n0 10690  df-z 10757  df-dec 10866  df-uz 10972  df-q 11064  df-rp 11102  df-xneg 11199  df-xadd 11200  df-xmul 11201  df-ioo 11414  df-ioc 11415  df-ico 11416  df-icc 11417  df-fz 11554  df-fzo 11665  df-fl 11758  df-mod 11825  df-seq 11923  df-exp 11982  df-fac 12168  df-bc 12195  df-hash 12220  df-shft 12673  df-cj 12705  df-re 12706  df-im 12707  df-sqr 12841  df-abs 12842  df-limsup 13066  df-clim 13083  df-rlim 13084  df-sum 13281  df-ef 13470  df-sin 13472  df-cos 13473  df-tan 13474  df-pi 13475  df-struct 14293  df-ndx 14294  df-slot 14295  df-base 14296  df-sets 14297  df-ress 14298  df-plusg 14369  df-mulr 14370  df-starv 14371  df-sca 14372  df-vsca 14373  df-ip 14374  df-tset 14375  df-ple 14376  df-ds 14378  df-unif 14379  df-hom 14380  df-cco 14381  df-rest 14479  df-topn 14480  df-0g 14498  df-gsum 14499  df-topgen 14500  df-pt 14501  df-prds 14504  df-xrs 14558  df-qtop 14563  df-imas 14564  df-xps 14566  df-mre 14642  df-mrc 14643  df-acs 14645  df-mnd 15533  df-submnd 15583  df-mulg 15666  df-cntz 15953  df-cmn 16399  df-psmet 17933  df-xmet 17934  df-met 17935  df-bl 17936  df-mopn 17937  df-fbas 17938  df-fg 17939  df-cnfld 17943  df-top 18634  df-bases 18636  df-topon 18637  df-topsp 18638  df-cld 18754  df-ntr 18755  df-cls 18756  df-nei 18833  df-lp 18871  df-perf 18872  df-cn 18962  df-cnp 18963  df-haus 19050  df-cmp 19121  df-tx 19266  df-hmeo 19459  df-fil 19550  df-fm 19642  df-flim 19643  df-flf 19644  df-xms 20026  df-ms 20027  df-tms 20028  df-cncf 20585  df-limc 21473  df-dv 21474  df-log 22140  df-cxp 22141

This theorem is referenced by:  resqrcn  22319