Theorem cxpcn3 20585

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 9047	. . . . . . . 8 |- 0 e. RR
2		pnfxr 10669	. . . . . . . 8 |- +oo e. RR*
3		icossre 10947	. . . . . . . 8 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
4	1, 2, 3	mp2an 654	. . . . . . 7 |- ( 0 [,) +oo ) C_ RR
5		ax-resscn 9003	. . . . . . 7 |- RR C_ CC
6	4, 5	sstri 3317	. . . . . 6 |- ( 0 [,) +oo ) C_ CC
7	6	sseli 3304	. . . . 5 |- ( x e. ( 0 [,) +oo ) -> x e. CC )
8		cxpcn3.d	. . . . . . 7 |- D = ( `' Re " RR+ )
9		cnvimass 5183	. . . . . . . 8 |- ( `' Re " RR+ ) C_ dom Re
10		ref 11872	. . . . . . . . 9 |- Re : CC --> RR
11	10	fdmi 5555	. . . . . . . 8 |- dom Re = CC
12	9, 11	sseqtri 3340	. . . . . . 7 |- ( `' Re " RR+ ) C_ CC
13	8, 12	eqsstri 3338	. . . . . 6 |- D C_ CC
14	13	sseli 3304	. . . . 5 |- ( y e. D -> y e. CC )
15		cxpcl 20518	. . . . 5 |- ( ( x e. CC /\ y e. CC ) -> ( x ^ c y ) e. CC )
16	7, 14, 15	syl2an 464	. . . 4 |- ( ( x e. ( 0 [,) +oo ) /\ y e. D ) -> ( x ^ c y ) e. CC )
17	16	rgen2 2762	. . 3 |- A. x e. ( 0 [,) +oo ) A. y e. D ( x ^ c y ) e. CC
18		eqid 2404	. . . 4 |- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) ) = ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) )
19	18	fmpt2 6377	. . 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 200	. 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 18770	. . . . . . . . . . . 12 |- J e. (TopOn ` CC )
23		rpre 10574	. . . . . . . . . . . . . . 15 |- ( x e. RR+ -> x e. RR )
24		rpge0 10580	. . . . . . . . . . . . . . 15 |- ( x e. RR+ -> 0 <_ x )
25		elrege0 10963	. . . . . . . . . . . . . . 15 |- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
26	23, 24, 25	sylanbrc 646	. . . . . . . . . . . . . 14 |- ( x e. RR+ -> x e. ( 0 [,) +oo ) )
27	26	ssriv 3312	. . . . . . . . . . . . 13 |- RR+ C_ ( 0 [,) +oo )
28	27, 6	sstri 3317	. . . . . . . . . . . 12 |- RR+ C_ CC
29		resttopon 17179	. . . . . . . . . . . 12 |- ( ( J e. (TopOn ` CC ) /\ RR+ C_ CC ) -> ( J ↾t RR+ ) e. (TopOn ` RR+ ) )
30	22, 28, 29	mp2an 654	. . . . . . . . . . 11 |- ( J ↾t RR+ ) e. (TopOn ` RR+ )
31	30	toponunii 16952	. . . . . . . . . . . 12 |- RR+ = U. ( J ↾t RR+ )
32	31	restid 13616	. . . . . . . . . . 11 |- ( ( J ↾t RR+ ) e. (TopOn ` RR+ ) -> ( ( J ↾t RR+ ) ↾t RR+ ) = ( J ↾t RR+ ) )
33	30, 32	ax-mp 8	. . . . . . . . . 10 |- ( ( J ↾t RR+ ) ↾t RR+ ) = ( J ↾t RR+ )
34	33	eqcomi 2408	. . . . . . . . 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 3327	. . . . . . . . . 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 2404	. . . . . . . . . . 11 |- ( J ↾t RR+ ) = ( J ↾t RR+ )
42	21, 41	cxpcn2 20583	. . . . . . . . . 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 17662	. . . . . . . 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 10963	. . . . . . . . . . . . 13 |- ( u e. ( 0 [,) +oo ) <-> ( u e. RR /\ 0 <_ u ) )
46	45	simplbi 447	. . . . . . . . . . . 12 |- ( u e. ( 0 [,) +oo ) -> u e. RR )
47	46	adantr 452	. . . . . . . . . . 11 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> u e. RR )
48	47	adantr 452	. . . . . . . . . 10 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> u e. RR )
49		simpr 448	. . . . . . . . . 10 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> 0 < u )
50	48, 49	elrpd 10602	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> u e. RR+ )
51		simplr 732	. . . . . . . . 9 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> v e. D )
52		opelxp 4867	. . . . . . . . 9 |- ( <. u , v >. e. ( RR+ X. D ) <-> ( u e. RR+ /\ v e. D ) )
53	50, 51, 52	sylanbrc 646	. . . . . . . 8 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 < u ) -> <. u , v >. e. ( RR+ X. D ) )
54		resttopon 17179	. . . . . . . . . . . . 13 |- ( ( J e. (TopOn ` CC ) /\ D C_ CC ) -> ( J ↾t D ) e. (TopOn ` D ) )
55	22, 13, 54	mp2an 654	. . . . . . . . . . . 12 |- ( J ↾t D ) e. (TopOn ` D )
56	38, 55	eqeltri 2474	. . . . . . . . . . 11 |- L e. (TopOn ` D )
57		txtopon 17576	. . . . . . . . . . 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 654	. . . . . . . . . 10 |- ( ( J ↾t RR+ ) tX L ) e. (TopOn ` ( RR+ X. D ) )
59	58	toponunii 16952	. . . . . . . . 9 |- ( RR+ X. D ) = U. ( ( J ↾t RR+ ) tX L )
60	59	cncnpi 17296	. . . . . . . 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 643	. . . . . . 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 3327	. . . . . . . 8 |- D C_ D
63		resmpt2 6127	. . . . . . . 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 654	. . . . . . 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 17179	. . . . . . . . . . . . 13 |- ( ( J e. (TopOn ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( J ↾t ( 0 [,) +oo ) ) e. (TopOn ` ( 0 [,) +oo ) ) )
67	22, 6, 66	mp2an 654	. . . . . . . . . . . 12 |- ( J ↾t ( 0 [,) +oo ) ) e. (TopOn ` ( 0 [,) +oo ) )
68	65, 67	eqeltri 2474	. . . . . . . . . . 11 |- K e. (TopOn ` ( 0 [,) +oo ) )
69		ioorp 10944	. . . . . . . . . . . . . 14 |- ( 0 (,) +oo ) = RR+
70		iooretop 18753	. . . . . . . . . . . . . 14 |- ( 0 (,) +oo ) e. ( topGen ` ran (,) )
71	69, 70	eqeltrri 2475	. . . . . . . . . . . . 13 |- RR+ e. ( topGen ` ran (,) )
72		retop 18748	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) e. Top
73		ovex 6065	. . . . . . . . . . . . . . 15 |- ( 0 [,) +oo ) e. _V
74		restopnb 17193	. . . . . . . . . . . . . . 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 664	. . . . . . . . . . . . . 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 1279	. . . . . . . . . . . . 13 |- ( RR+ e. ( topGen ` ran (,) ) <-> RR+ e. ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) ) )
77	71, 76	mpbi 200	. . . . . . . . . . . 12 |- RR+ e. ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) )
78		eqid 2404	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
79	21, 78	rerest 18788	. . . . . . . . . . . . . 14 |- ( ( 0 [,) +oo ) C_ RR -> ( J ↾t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) ) )
80	4, 79	ax-mp 8	. . . . . . . . . . . . 13 |- ( J ↾t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) )
81	65, 80	eqtri 2424	. . . . . . . . . . . 12 |- K = ( ( topGen ` ran (,) ) ↾t ( 0 [,) +oo ) )
82	77, 81	eleqtrri 2477	. . . . . . . . . . 11 |- RR+ e. K
83		toponmax 16948	. . . . . . . . . . . 12 |- ( L e. (TopOn ` D ) -> D e. L )
84	56, 83	ax-mp 8	. . . . . . . . . . 11 |- D e. L
85		txrest 17616	. . . . . . . . . . 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 655	. . . . . . . . . 10 |- ( ( K tX L ) ↾t ( RR+ X. D ) ) = ( ( K ↾t RR+ ) tX ( L ↾t D ) )
87	65	oveq1i 6050	. . . . . . . . . . . 12 |- ( K ↾t RR+ ) = ( ( J ↾t ( 0 [,) +oo ) ) ↾t RR+ )
88		restabs 17183	. . . . . . . . . . . . 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 1279	. . . . . . . . . . . 12 |- ( ( J ↾t ( 0 [,) +oo ) ) ↾t RR+ ) = ( J ↾t RR+ )
90	87, 89	eqtri 2424	. . . . . . . . . . 11 |- ( K ↾t RR+ ) = ( J ↾t RR+ )
91	56	toponunii 16952	. . . . . . . . . . . . 13 |- D = U. L
92	91	restid 13616	. . . . . . . . . . . 12 |- ( L e. (TopOn ` D ) -> ( L ↾t D ) = L )
93	56, 92	ax-mp 8	. . . . . . . . . . 11 |- ( L ↾t D ) = L
94	90, 93	oveq12i 6052	. . . . . . . . . 10 |- ( ( K ↾t RR+ ) tX ( L ↾t D ) ) = ( ( J ↾t RR+ ) tX L )
95	86, 94	eqtri 2424	. . . . . . . . 9 |- ( ( K tX L ) ↾t ( RR+ X. D ) ) = ( ( J ↾t RR+ ) tX L )
96	95	oveq1i 6050	. . . . . . . 8 |- ( ( ( K tX L ) ↾t ( RR+ X. D ) ) CnP J ) = ( ( ( J ↾t RR+ ) tX L ) CnP J )
97	96	fveq1i 5688	. . . . . . 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 2487	. . . . . 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 17576	. . . . . . . . . 10 |- ( ( K e. (TopOn ` ( 0 [,) +oo ) ) /\ L e. (TopOn ` D ) ) -> ( K tX L ) e. (TopOn ` ( ( 0 [,) +oo ) X. D ) ) )
100	68, 56, 99	mp2an 654	. . . . . . . . 9 |- ( K tX L ) e. (TopOn ` ( ( 0 [,) +oo ) X. D ) )
101	100	topontopi 16951	. . . . . . . 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 4943	. . . . . . . 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 17587	. . . . . . . . . 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 655	. . . . . . . . 9 |- ( RR+ X. D ) e. ( K tX L )
107		isopn3i 17101	. . . . . . . . 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 654	. . . . . . . 8 |- ( ( int ` ( K tX L ) ) ` ( RR+ X. D ) ) = ( RR+ X. D )
109	53, 108	syl6eleqr 2495	. . . . . . 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 16951	. . . . . . . . 9 |- K e. Top
112	56	topontopi 16951	. . . . . . . . 9 |- L e. Top
113	68	toponunii 16952	. . . . . . . . 9 |- ( 0 [,) +oo ) = U. K
114	111, 112, 113, 91	txunii 17578	. . . . . . . 8 |- ( ( 0 [,) +oo ) X. D ) = U. ( K tX L )
115	22	toponunii 16952	. . . . . . . 8 |- CC = U. J
116	114, 115	cnprest 17307	. . . . . . 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 1185	. . . . . 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 224	. . . . 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 2404	. . . . . . . . . . 11 |- ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 ) = ( if ( ( Re ` v ) <_ 1 , ( Re ` v ) , 1 ) / 2 )
121		eqid 2404	. . . . . . . . . . 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 20584	. . . . . . . . . 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 2749	. . . . . . . . 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		0le0 10037	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 0
125		elrege0 10963	. . . . . . . . . . . . . . . . . . 19 |- ( 0 e. ( 0 [,) +oo ) <-> ( 0 e. RR /\ 0 <_ 0 ) )
126	1, 124, 125	mpbir2an 887	. . . . . . . . . . . . . . . . . 18 |- 0 e. ( 0 [,) +oo )
127	126	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> 0 e. ( 0 [,) +oo ) )
128		simprl 733	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> a e. ( 0 [,) +oo ) )
129	127, 128	ovresd 6173	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) = ( 0 ( abs o. - ) a ) )
130		0cn 9040	. . . . . . . . . . . . . . . . 17 |- 0 e. CC
131	6, 128	sseldi 3306	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> a e. CC )
132		eqid 2404	. . . . . . . . . . . . . . . . . 18 |- ( abs o. - ) = ( abs o. - )
133	132	cnmetdval 18758	. . . . . . . . . . . . . . . . 17 |- ( ( 0 e. CC /\ a e. CC ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
134	130, 131, 133	sylancr 645	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
135		df-neg 9250	. . . . . . . . . . . . . . . . . 18 |- -u a = ( 0 - a )
136	135	fveq2i 5690	. . . . . . . . . . . . . . . . 17 |- ( abs ` -u a ) = ( abs ` ( 0 - a ) )
137	131	absnegd 12206	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` -u a ) = ( abs ` a ) )
138	136, 137	syl5eqr 2450	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` ( 0 - a ) ) = ( abs ` a ) )
139	129, 134, 138	3eqtrd 2440	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) = ( abs ` a ) )
140	139	breq1d 4182	. . . . . . . . . . . . . 14 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( 0 ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) a ) < d <-> ( abs ` a ) < d ) )
141		simpl 444	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> v e. D )
142		simprr 734	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> b e. D )
143	141, 142	ovresd 6173	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( ( abs o. - ) |` ( D X. D ) ) b ) = ( v ( abs o. - ) b ) )
144	13, 141	sseldi 3306	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> v e. CC )
145	13, 142	sseldi 3306	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> b e. CC )
146	132	cnmetdval 18758	. . . . . . . . . . . . . . . . 17 |- ( ( v e. CC /\ b e. CC ) -> ( v ( abs o. - ) b ) = ( abs ` ( v - b ) ) )
147	144, 145, 146	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( abs o. - ) b ) = ( abs ` ( v - b ) ) )
148	143, 147	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( v ( ( abs o. - ) |` ( D X. D ) ) b ) = ( abs ` ( v - b ) ) )
149	148	breq1d 4182	. . . . . . . . . . . . . 14 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( ( v ( ( abs o. - ) |` ( D X. D ) ) b ) < d <-> ( abs ` ( v - b ) ) < d ) )
150	140, 149	anbi12d 692	. . . . . . . . . . . . 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 ) ) )
151		oveq12 6049	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = 0 /\ y = v ) -> ( x ^ c y ) = ( 0 ^ c v ) )
152		ovex 6065	. . . . . . . . . . . . . . . . . . 19 |- ( 0 ^ c v ) e. _V
153	151, 18, 152	ovmpt2a 6163	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) ) v ) = ( 0 ^ c v ) )
154	126, 141, 153	sylancr 645	. . . . . . . . . . . . . . . . 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 ) )
155	8	eleq2i 2468	. . . . . . . . . . . . . . . . . . . . 21 |- ( v e. D <-> v e. ( `' Re " RR+ ) )
156		ffn 5550	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Re : CC --> RR -> Re Fn CC )
157		elpreima 5809	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Re Fn CC -> ( v e. ( `' Re " RR+ ) <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) ) )
158	10, 156, 157	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 |- ( v e. ( `' Re " RR+ ) <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) )
159	155, 158	bitri 241	. . . . . . . . . . . . . . . . . . . 20 |- ( v e. D <-> ( v e. CC /\ ( Re ` v ) e. RR+ ) )
160	159	simplbi 447	. . . . . . . . . . . . . . . . . . 19 |- ( v e. D -> v e. CC )
161	159	simprbi 451	. . . . . . . . . . . . . . . . . . . . 21 |- ( v e. D -> ( Re ` v ) e. RR+ )
162	161	rpne0d 10609	. . . . . . . . . . . . . . . . . . . 20 |- ( v e. D -> ( Re ` v ) =/= 0 )
163		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( v = 0 -> ( Re ` v ) = ( Re ` 0 ) )
164		re0 11912	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Re ` 0 ) = 0
165	163, 164	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . 21 |- ( v = 0 -> ( Re ` v ) = 0 )
166	165	necon3i 2606	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Re ` v ) =/= 0 -> v =/= 0 )
167	162, 166	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( v e. D -> v =/= 0 )
168	160, 167	0cxpd 20554	. . . . . . . . . . . . . . . . . 18 |- ( v e. D -> ( 0 ^ c v ) = 0 )
169	168	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ^ c v ) = 0 )
170	154, 169	eqtrd 2436	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) ) v ) = 0 )
171		oveq12 6049	. . . . . . . . . . . . . . . . . 18 |- ( ( x = a /\ y = b ) -> ( x ^ c y ) = ( a ^ c b ) )
172		ovex 6065	. . . . . . . . . . . . . . . . . 18 |- ( a ^ c b ) e. _V
173	171, 18, 172	ovmpt2a 6163	. . . . . . . . . . . . . . . . 17 |- ( ( a e. ( 0 [,) +oo ) /\ b e. D ) -> ( a ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) ) b ) = ( a ^ c b ) )
174	173	adantl 453	. . . . . . . . . . . . . . . 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 ) )
175	170, 174	oveq12d 6058	. . . . . . . . . . . . . . 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 ) ) )
176	131, 145	cxpcld 20552	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( a ^ c b ) e. CC )
177	132	cnmetdval 18758	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. CC /\ ( a ^ c b ) e. CC ) -> ( 0 ( abs o. - ) ( a ^ c b ) ) = ( abs ` ( 0 - ( a ^ c b ) ) ) )
178	130, 176, 177	sylancr 645	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( 0 ( abs o. - ) ( a ^ c b ) ) = ( abs ` ( 0 - ( a ^ c b ) ) ) )
179		df-neg 9250	. . . . . . . . . . . . . . . . 17 |- -u ( a ^ c b ) = ( 0 - ( a ^ c b ) )
180	179	fveq2i 5690	. . . . . . . . . . . . . . . 16 |- ( abs ` -u ( a ^ c b ) ) = ( abs ` ( 0 - ( a ^ c b ) ) )
181	176	absnegd 12206	. . . . . . . . . . . . . . . 16 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` -u ( a ^ c b ) ) = ( abs ` ( a ^ c b ) ) )
182	180, 181	syl5eqr 2450	. . . . . . . . . . . . . . 15 |- ( ( v e. D /\ ( a e. ( 0 [,) +oo ) /\ b e. D ) ) -> ( abs ` ( 0 - ( a ^ c b ) ) ) = ( abs ` ( a ^ c b ) ) )
183	175, 178, 182	3eqtrd 2440	. . . . . . . . . . . . . 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 ) ) )
184	183	breq1d 4182	. . . . . . . . . . . . 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 ) )
185	150, 184	imbi12d 312	. . . . . . . . . . . 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 ) ) )
186	185	2ralbidva 2706	. . . . . . . . . . 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 ) ) )
187	186	rexbidv 2687	. . . . . . . . . 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 ) ) )
188	187	ralbidv 2686	. . . . . . . . 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 ) ) )
189	123, 188	mpbird 224	. . . . . . . 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 ) )
190		cnxmet 18760	. . . . . . . . . . 11 |- ( abs o. - ) e. ( * Met ` CC )
191	190	a1i 11	. . . . . . . . . 10 |- ( v e. D -> ( abs o. - ) e. ( * Met ` CC ) )
192		xmetres2 18344	. . . . . . . . . 10 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( * Met ` ( 0 [,) +oo ) ) )
193	191, 6, 192	sylancl 644	. . . . . . . . 9 |- ( v e. D -> ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) e. ( * Met ` ( 0 [,) +oo ) ) )
194		xmetres2 18344	. . . . . . . . . 10 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ D C_ CC ) -> ( ( abs o. - ) |` ( D X. D ) ) e. ( * Met ` D ) )
195	191, 13, 194	sylancl 644	. . . . . . . . 9 |- ( v e. D -> ( ( abs o. - ) |` ( D X. D ) ) e. ( * Met ` D ) )
196	126	a1i 11	. . . . . . . . 9 |- ( v e. D -> 0 e. ( 0 [,) +oo ) )
197		id 20	. . . . . . . . 9 |- ( v e. D -> v e. D )
198		eqid 2404	. . . . . . . . . . . . 13 |- ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) = ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) )
199	21	cnfldtopn 18769	. . . . . . . . . . . . 13 |- J = ( MetOpen ` ( abs o. - ) )
200		eqid 2404	. . . . . . . . . . . . 13 |- ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
201	198, 199, 200	metrest 18507	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( J ↾t ( 0 [,) +oo ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) ) )
202	190, 6, 201	mp2an 654	. . . . . . . . . . 11 |- ( J ↾t ( 0 [,) +oo ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
203	65, 202	eqtri 2424	. . . . . . . . . 10 |- K = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,) +oo ) X. ( 0 [,) +oo ) ) ) )
204		eqid 2404	. . . . . . . . . . . . 13 |- ( ( abs o. - ) |` ( D X. D ) ) = ( ( abs o. - ) |` ( D X. D ) )
205		eqid 2404	. . . . . . . . . . . . 13 |- ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
206	204, 199, 205	metrest 18507	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ D C_ CC ) -> ( J ↾t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) )
207	190, 13, 206	mp2an 654	. . . . . . . . . . 11 |- ( J ↾t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
208	38, 207	eqtri 2424	. . . . . . . . . 10 |- L = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
209	203, 208, 199	txmetcnp 18530	. . . . . . . . 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 ) ) ) )
210	193, 195, 191, 196, 197, 209	syl32anc 1192	. . . . . . . 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 ) ) ) )
211	119, 189, 210	mpbir2and 889	. . . . . . 7 |- ( v e. D -> ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) ) e. ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) )
212	211	ad2antlr 708	. . . . . 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 >. ) )
213		simpr 448	. . . . . . . 8 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> 0 = u )
214	213	opeq1d 3950	. . . . . . 7 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> <. 0 , v >. = <. u , v >. )
215	214	fveq2d 5691	. . . . . 6 |- ( ( ( u e. ( 0 [,) +oo ) /\ v e. D ) /\ 0 = u ) -> ( ( ( K tX L ) CnP J ) ` <. 0 , v >. ) = ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
216	212, 215	eleqtrd 2480	. . . . 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 >. ) )
217	45	simprbi 451	. . . . . . 7 |- ( u e. ( 0 [,) +oo ) -> 0 <_ u )
218	217	adantr 452	. . . . . 6 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> 0 <_ u )
219		leloe 9117	. . . . . . 7 |- ( ( 0 e. RR /\ u e. RR ) -> ( 0 <_ u <-> ( 0 < u \/ 0 = u ) ) )
220	1, 47, 219	sylancr 645	. . . . . 6 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 <_ u <-> ( 0 < u \/ 0 = u ) ) )
221	218, 220	mpbid 202	. . . . 5 |- ( ( u e. ( 0 [,) +oo ) /\ v e. D ) -> ( 0 < u \/ 0 = u ) )
222	118, 216, 221	mpjaodan 762	. . . 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 >. ) )
223	222	rgen2 2762	. . 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 >. )
224		fveq2 5687	. . . . 5 |- ( z = <. u , v >. -> ( ( ( K tX L ) CnP J ) ` z ) = ( ( ( K tX L ) CnP J ) ` <. u , v >. ) )
225	224	eleq2d 2471	. . . 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 >. ) ) )
226	225	ralxp 4975	. . 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 >. ) )
227	223, 226	mpbir 201	. 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 )
228		cncnp 17298	. . 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 ) ) ) )
229	100, 22, 228	mp2an 654	. 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 ) ) )
230	20, 227, 229	mpbir2an 887	1 |- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^ c y ) ) e. ( ( K tX L ) Cn J )

Syntax hints:   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   C_ wss 3280   ifcif 3699   <.cop 3777   class class class wbr 4172   X. cxp 4835   `'ccnv 4836   dom cdm 4837   ran crn 4838   |` cres 4839   "cima 4840   o. ccom 4841   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   e. cmpt2 6042   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   +oocpnf 9073   RR*cxr 9075   < clt 9076   <_ cle 9077   - cmin 9247   -ucneg 9248   / cdiv 9633   2c2 10005   RR+crp 10568   (,)cioo 10872   [,)cico 10874   Recre 11857   abscabs 11994   ↾_t crest 13603   TopOpenctopn 13604   topGenctg 13620   * Metcxmt 16641   MetOpencmopn 16646  ℂ_fldccnfld 16658   Topctop 16913  TopOnctopon 16914   intcnt 17036   Cn ccn 17242   CnP ccnp 17243   tX ctx 17545   ^ c ccxp 20406

This theorem is referenced by:  resqrcn  20586

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ioc 10877  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-shft 11837  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-ef 12625  df-sin 12627  df-cos 12628  df-tan 12629  df-pi 12630  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-fbas 16654  df-fg 16655  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-lp 17155  df-perf 17156  df-cn 17245  df-cnp 17246  df-haus 17333  df-cmp 17404  df-tx 17547  df-hmeo 17740  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-limc 19706  df-dv 19707  df-log 20407  df-cxp 20408