Theorem cxpcn3lem 23552

Description: Lemma for cxpcn3 23553. (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 )
cxpcn3.u	|- U = ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 )
cxpcn3.t	|- T = if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) )

Assertion

Ref	Expression
cxpcn3lem	|- ( ( A e. D /\ E e. RR+ ) -> E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < E ) )

Distinct variable groups:   a, b, d, A   E, a, b, d   J, d   K, a, b, d   D, a, b, d   L, a, b, d   T, a, b, d

Allowed substitution hints:   U( a, b, d)   J( a, b)

Proof of Theorem cxpcn3lem

Step	Hyp	Ref	Expression
1		cxpcn3.t	. . 3 |- T = if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) )
2		cxpcn3.u	. . . . 5 |- U = ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 )
3		cxpcn3.d	. . . . . . . . . . 11 |- D = ( `' Re " RR+ )
4	3	eleq2i 2507	. . . . . . . . . 10 |- ( A e. D <-> A e. ( `' Re " RR+ ) )
5		ref 13154	. . . . . . . . . . 11 |- Re : CC --> RR
6		ffn 5746	. . . . . . . . . . 11 |- ( Re : CC --> RR -> Re Fn CC )
7		elpreima 6017	. . . . . . . . . . 11 |- ( Re Fn CC -> ( A e. ( `' Re " RR+ ) <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) ) )
8	5, 6, 7	mp2b 10	. . . . . . . . . 10 |- ( A e. ( `' Re " RR+ ) <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) )
9	4, 8	bitri 252	. . . . . . . . 9 |- ( A e. D <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) )
10	9	simprbi 465	. . . . . . . 8 |- ( A e. D -> ( Re ` A ) e. RR+ )
11	10	adantr 466	. . . . . . 7 |- ( ( A e. D /\ E e. RR+ ) -> ( Re ` A ) e. RR+ )
12		1rp 11306	. . . . . . 7 |- 1 e. RR+
13		ifcl 3957	. . . . . . 7 |- ( ( ( Re ` A ) e. RR+ /\ 1 e. RR+ ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
14	11, 12, 13	sylancl 666	. . . . . 6 |- ( ( A e. D /\ E e. RR+ ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
15	14	rphalfcld 11353	. . . . 5 |- ( ( A e. D /\ E e. RR+ ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) e. RR+ )
16	2, 15	syl5eqel 2521	. . . 4 |- ( ( A e. D /\ E e. RR+ ) -> U e. RR+ )
17		simpr 462	. . . . 5 |- ( ( A e. D /\ E e. RR+ ) -> E e. RR+ )
18	16	rpreccld 11351	. . . . . 6 |- ( ( A e. D /\ E e. RR+ ) -> ( 1 / U ) e. RR+ )
19	18	rpred 11341	. . . . 5 |- ( ( A e. D /\ E e. RR+ ) -> ( 1 / U ) e. RR )
20	17, 19	rpcxpcld 23540	. . . 4 |- ( ( A e. D /\ E e. RR+ ) -> ( E ^c ( 1 / U ) ) e. RR+ )
21	16, 20	ifcld 3958	. . 3 |- ( ( A e. D /\ E e. RR+ ) -> if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) e. RR+ )
22	1, 21	syl5eqel 2521	. 2 |- ( ( A e. D /\ E e. RR+ ) -> T e. RR+ )
23		elrege0 11737	. . . 4 |- ( a e. ( 0 [,) +oo ) <-> ( a e. RR /\ 0 <_ a ) )
24		0red 9643	. . . . . . 7 |- ( ( A e. D /\ E e. RR+ ) -> 0 e. RR )
25		leloe 9719	. . . . . . 7 |- ( ( 0 e. RR /\ a e. RR ) -> ( 0 <_ a <-> ( 0 < a \/ 0 = a ) ) )
26	24, 25	sylan 473	. . . . . 6 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( 0 <_ a <-> ( 0 < a \/ 0 = a ) ) )
27		elrp 11304	. . . . . . . . 9 |- ( a e. RR+ <-> ( a e. RR /\ 0 < a ) )
28		simp2l 1031	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a e. RR+ )
29		simp2r 1032	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> b e. D )
30		cnvimass 5208	. . . . . . . . . . . . . . . . . 18 |- ( `' Re " RR+ ) C_ dom Re
31	5	fdmi 5751	. . . . . . . . . . . . . . . . . 18 |- dom Re = CC
32	30, 31	sseqtri 3502	. . . . . . . . . . . . . . . . 17 |- ( `' Re " RR+ ) C_ CC
33	3, 32	eqsstri 3500	. . . . . . . . . . . . . . . 16 |- D C_ CC
34	33	sseli 3466	. . . . . . . . . . . . . . 15 |- ( b e. D -> b e. CC )
35	29, 34	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> b e. CC )
36		abscxp 23502	. . . . . . . . . . . . . 14 |- ( ( a e. RR+ /\ b e. CC ) -> ( abs ` ( a ^c b ) ) = ( a ^c ( Re ` b ) ) )
37	28, 35, 36	syl2anc 665	. . . . . . . . . . . . 13 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( a ^c b ) ) = ( a ^c ( Re ` b ) ) )
38	35	recld 13236	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` b ) e. RR )
39	28, 38	rpcxpcld 23540	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( Re ` b ) ) e. RR+ )
40	39	rpred 11341	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( Re ` b ) ) e. RR )
41	16	3ad2ant1 1026	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U e. RR+ )
42	41	rpred 11341	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U e. RR )
43	28, 42	rpcxpcld 23540	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c U ) e. RR+ )
44	43	rpred 11341	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c U ) e. RR )
45		simp1r 1030	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> E e. RR+ )
46	45	rpred 11341	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> E e. RR )
47		simp1l 1029	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> A e. D )
48	9	simplbi 461	. . . . . . . . . . . . . . . . . . 19 |- ( A e. D -> A e. CC )
49	47, 48	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> A e. CC )
50	49	recld 13236	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` A ) e. RR )
51	50	rehalfcld 10859	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( Re ` A ) / 2 ) e. RR )
52		1re 9641	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
53		min1 11483	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ ( Re ` A ) )
54	50, 52, 53	sylancl 666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ ( Re ` A ) )
55	14	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
56	55	rpred 11341	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR )
57		2re 10679	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
58	57	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> 2 e. RR )
59		2pos 10701	. . . . . . . . . . . . . . . . . . . 20 |- 0 < 2
60	59	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> 0 < 2 )
61		lediv1 10469	. . . . . . . . . . . . . . . . . . 19 |- ( ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR /\ ( Re ` A ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ ( Re ` A ) <-> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) <_ ( ( Re ` A ) / 2 ) ) )
62	56, 50, 58, 60, 61	syl112anc 1268	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ ( Re ` A ) <-> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) <_ ( ( Re ` A ) / 2 ) ) )
63	54, 62	mpbid 213	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) <_ ( ( Re ` A ) / 2 ) )
64	2, 63	syl5eqbr 4459	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U <_ ( ( Re ` A ) / 2 ) )
65	50	recnd 9668	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` A ) e. CC )
66	65	2halvesd 10858	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( ( Re ` A ) / 2 ) + ( ( Re ` A ) / 2 ) ) = ( Re ` A ) )
67	49, 35	resubd 13258	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) = ( ( Re ` A ) - ( Re ` b ) ) )
68	49, 35	subcld 9985	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( A - b ) e. CC )
69	68	recld 13236	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) e. RR )
70	68	abscld 13476	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) e. RR )
71	68	releabsd 13491	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) <_ ( abs ` ( A - b ) ) )
72		simp3r 1034	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) < T )
73	72, 1	syl6breq 4465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) < if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) )
74	20	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( E ^c ( 1 / U ) ) e. RR+ )
75	74	rpred 11341	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( E ^c ( 1 / U ) ) e. RR )
76		ltmin 11488	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( abs ` ( A - b ) ) e. RR /\ U e. RR /\ ( E ^c ( 1 / U ) ) e. RR ) -> ( ( abs ` ( A - b ) ) < if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) <-> ( ( abs ` ( A - b ) ) < U /\ ( abs ` ( A - b ) ) < ( E ^c ( 1 / U ) ) ) ) )
77	70, 42, 75, 76	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( abs ` ( A - b ) ) < if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) <-> ( ( abs ` ( A - b ) ) < U /\ ( abs ` ( A - b ) ) < ( E ^c ( 1 / U ) ) ) ) )
78	73, 77	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( abs ` ( A - b ) ) < U /\ ( abs ` ( A - b ) ) < ( E ^c ( 1 / U ) ) ) )
79	78	simpld 460	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) < U )
80	69, 70, 42, 71, 79	lelttrd 9792	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) < U )
81	69, 42, 51, 80, 64	ltletrd 9794	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) < ( ( Re ` A ) / 2 ) )
82	67, 81	eqbrtrrd 4448	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( Re ` A ) - ( Re ` b ) ) < ( ( Re ` A ) / 2 ) )
83	50, 38, 51	ltsubadd2d 10210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( ( Re ` A ) - ( Re ` b ) ) < ( ( Re ` A ) / 2 ) <-> ( Re ` A ) < ( ( Re ` b ) + ( ( Re ` A ) / 2 ) ) ) )
84	82, 83	mpbid 213	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` A ) < ( ( Re ` b ) + ( ( Re ` A ) / 2 ) ) )
85	66, 84	eqbrtrd 4446	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( ( Re ` A ) / 2 ) + ( ( Re ` A ) / 2 ) ) < ( ( Re ` b ) + ( ( Re ` A ) / 2 ) ) )
86	51, 38, 51	ltadd1d 10205	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( ( Re ` A ) / 2 ) < ( Re ` b ) <-> ( ( ( Re ` A ) / 2 ) + ( ( Re ` A ) / 2 ) ) < ( ( Re ` b ) + ( ( Re ` A ) / 2 ) ) ) )
87	85, 86	mpbird 235	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( Re ` A ) / 2 ) < ( Re ` b ) )
88	42, 51, 38, 64, 87	lelttrd 9792	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U < ( Re ` b ) )
89	28	rpred 11341	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a e. RR )
90	52	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> 1 e. RR )
91	28	rprege0d 11348	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a e. RR /\ 0 <_ a ) )
92		absid 13338	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. RR /\ 0 <_ a ) -> ( abs ` a ) = a )
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` a ) = a )
94		simp3l 1033	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` a ) < T )
95	93, 94	eqbrtrrd 4448	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < T )
96	95, 1	syl6breq 4465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) )
97		ltmin 11488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ U e. RR /\ ( E ^c ( 1 / U ) ) e. RR ) -> ( a < if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) <-> ( a < U /\ a < ( E ^c ( 1 / U ) ) ) ) )
98	89, 42, 75, 97	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a < if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) <-> ( a < U /\ a < ( E ^c ( 1 / U ) ) ) ) )
99	96, 98	mpbid 213	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a < U /\ a < ( E ^c ( 1 / U ) ) ) )
100	99	simpld 460	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < U )
101		rehalfcl 10839	. . . . . . . . . . . . . . . . . . 19 |- ( 1 e. RR -> ( 1 / 2 ) e. RR )
102	52, 101	mp1i 13	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / 2 ) e. RR )
103		min2 11484	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ 1 )
104	50, 52, 103	sylancl 666	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ 1 )
105		lediv1 10469	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ 1 <-> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) <_ ( 1 / 2 ) ) )
106	56, 90, 58, 60, 105	syl112anc 1268	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ 1 <-> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) <_ ( 1 / 2 ) ) )
107	104, 106	mpbid 213	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) <_ ( 1 / 2 ) )
108	2, 107	syl5eqbr 4459	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U <_ ( 1 / 2 ) )
109		halflt1 10831	. . . . . . . . . . . . . . . . . . 19 |- ( 1 / 2 ) < 1
110	109	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / 2 ) < 1 )
111	42, 102, 90, 108, 110	lelttrd 9792	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U < 1 )
112	89, 42, 90, 100, 111	lttrd 9795	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < 1 )
113	28, 42, 112, 38	cxplt3d 23542	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( U < ( Re ` b ) <-> ( a ^c ( Re ` b ) ) < ( a ^c U ) ) )
114	88, 113	mpbid 213	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( Re ` b ) ) < ( a ^c U ) )
115	41	rpcnne0d 11350	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( U e. CC /\ U =/= 0 ) )
116		recid 10283	. . . . . . . . . . . . . . . . . . 19 |- ( ( U e. CC /\ U =/= 0 ) -> ( U x. ( 1 / U ) ) = 1 )
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( U x. ( 1 / U ) ) = 1 )
118	117	oveq2d 6321	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( U x. ( 1 / U ) ) ) = ( a ^c 1 ) )
119	41	rpreccld 11351	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / U ) e. RR+ )
120	119	rpcnd 11343	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / U ) e. CC )
121	28, 42, 120	cxpmuld 23544	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( U x. ( 1 / U ) ) ) = ( ( a ^c U ) ^c ( 1 / U ) ) )
122	28	rpcnd 11343	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a e. CC )
123	122	cxp1d 23516	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c 1 ) = a )
124	118, 121, 123	3eqtr3d 2478	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( a ^c U ) ^c ( 1 / U ) ) = a )
125	99	simprd 464	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < ( E ^c ( 1 / U ) ) )
126	124, 125	eqbrtrd 4446	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( a ^c U ) ^c ( 1 / U ) ) < ( E ^c ( 1 / U ) ) )
127	43	rprege0d 11348	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( a ^c U ) e. RR /\ 0 <_ ( a ^c U ) ) )
128	45	rprege0d 11348	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( E e. RR /\ 0 <_ E ) )
129		cxplt2 23508	. . . . . . . . . . . . . . . 16 |- ( ( ( ( a ^c U ) e. RR /\ 0 <_ ( a ^c U ) ) /\ ( E e. RR /\ 0 <_ E ) /\ ( 1 / U ) e. RR+ ) -> ( ( a ^c U ) < E <-> ( ( a ^c U ) ^c ( 1 / U ) ) < ( E ^c ( 1 / U ) ) ) )
130	127, 128, 119, 129	syl3anc 1264	. . . . . . . . . . . . . . 15 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( a ^c U ) < E <-> ( ( a ^c U ) ^c ( 1 / U ) ) < ( E ^c ( 1 / U ) ) ) )
131	126, 130	mpbird 235	. . . . . . . . . . . . . 14 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c U ) < E )
132	40, 44, 46, 114, 131	lttrd 9795	. . . . . . . . . . . . 13 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( Re ` b ) ) < E )
133	37, 132	eqbrtrd 4446	. . . . . . . . . . . 12 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( a ^c b ) ) < E )
134	133	3expia 1207	. . . . . . . . . . 11 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) ) -> ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
135	134	anassrs 652	. . . . . . . . . 10 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR+ ) /\ b e. D ) -> ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
136	135	ralrimiva 2846	. . . . . . . . 9 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR+ ) -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
137	27, 136	sylan2br 478	. . . . . . . 8 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR /\ 0 < a ) ) -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
138	137	expr 618	. . . . . . 7 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( 0 < a -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
139		elpreima 6017	. . . . . . . . . . . . . . . . . . 19 |- ( Re Fn CC -> ( b e. ( `' Re " RR+ ) <-> ( b e. CC /\ ( Re ` b ) e. RR+ ) ) )
140	5, 6, 139	mp2b 10	. . . . . . . . . . . . . . . . . 18 |- ( b e. ( `' Re " RR+ ) <-> ( b e. CC /\ ( Re ` b ) e. RR+ ) )
141	140	simprbi 465	. . . . . . . . . . . . . . . . 17 |- ( b e. ( `' Re " RR+ ) -> ( Re ` b ) e. RR+ )
142	141, 3	eleq2s 2537	. . . . . . . . . . . . . . . 16 |- ( b e. D -> ( Re ` b ) e. RR+ )
143	142	rpne0d 11346	. . . . . . . . . . . . . . 15 |- ( b e. D -> ( Re ` b ) =/= 0 )
144		fveq2 5881	. . . . . . . . . . . . . . . . 17 |- ( b = 0 -> ( Re ` b ) = ( Re ` 0 ) )
145		re0 13194	. . . . . . . . . . . . . . . . 17 |- ( Re ` 0 ) = 0
146	144, 145	syl6eq 2486	. . . . . . . . . . . . . . . 16 |- ( b = 0 -> ( Re ` b ) = 0 )
147	146	necon3i 2671	. . . . . . . . . . . . . . 15 |- ( ( Re ` b ) =/= 0 -> b =/= 0 )
148	143, 147	syl 17	. . . . . . . . . . . . . 14 |- ( b e. D -> b =/= 0 )
149	34, 148	0cxpd 23520	. . . . . . . . . . . . 13 |- ( b e. D -> ( 0 ^c b ) = 0 )
150	149	adantl 467	. . . . . . . . . . . 12 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 ^c b ) = 0 )
151	150	abs00bd 13333	. . . . . . . . . . 11 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( abs ` ( 0 ^c b ) ) = 0 )
152		simpllr 767	. . . . . . . . . . . 12 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> E e. RR+ )
153	152	rpgt0d 11344	. . . . . . . . . . 11 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> 0 < E )
154	151, 153	eqbrtrd 4446	. . . . . . . . . 10 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( abs ` ( 0 ^c b ) ) < E )
155		oveq1 6312	. . . . . . . . . . . 12 |- ( 0 = a -> ( 0 ^c b ) = ( a ^c b ) )
156	155	fveq2d 5885	. . . . . . . . . . 11 |- ( 0 = a -> ( abs ` ( 0 ^c b ) ) = ( abs ` ( a ^c b ) ) )
157	156	breq1d 4436	. . . . . . . . . 10 |- ( 0 = a -> ( ( abs ` ( 0 ^c b ) ) < E <-> ( abs ` ( a ^c b ) ) < E ) )
158	154, 157	syl5ibcom 223	. . . . . . . . 9 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 = a -> ( abs ` ( a ^c b ) ) < E ) )
159	158	a1dd 47	. . . . . . . 8 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 = a -> ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
160	159	ralrimdva 2850	. . . . . . 7 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( 0 = a -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
161	138, 160	jaod 381	. . . . . 6 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( ( 0 < a \/ 0 = a ) -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
162	26, 161	sylbid 218	. . . . 5 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( 0 <_ a -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
163	162	expimpd 606	. . . 4 |- ( ( A e. D /\ E e. RR+ ) -> ( ( a e. RR /\ 0 <_ a ) -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
164	23, 163	syl5bi 220	. . 3 |- ( ( A e. D /\ E e. RR+ ) -> ( a e. ( 0 [,) +oo ) -> A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
165	164	ralrimiv 2844	. 2 |- ( ( A e. D /\ E e. RR+ ) -> A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
166		breq2 4430	. . . . . 6 |- ( d = T -> ( ( abs ` a ) < d <-> ( abs ` a ) < T ) )
167		breq2 4430	. . . . . 6 |- ( d = T -> ( ( abs ` ( A - b ) ) < d <-> ( abs ` ( A - b ) ) < T ) )
168	166, 167	anbi12d 715	. . . . 5 |- ( d = T -> ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) <-> ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) )
169	168	imbi1d 318	. . . 4 |- ( d = T -> ( ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < E ) <-> ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
170	169	2ralbidv 2876	. . 3 |- ( d = T -> ( A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < E ) <-> A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) )
171	170	rspcev 3188	. 2 |- ( ( T e. RR+ /\ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) ) -> E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < E ) )
172	22, 165, 171	syl2anc 665	1 |- ( ( A e. D /\ E e. RR+ ) -> E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < E ) )

Syntax hints:   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   =/= wne 2625   A.wral 2782   E.wrex 2783   ifcif 3915   class class class wbr 4426   `'ccnv 4853   dom cdm 4854   "cima 4857   Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6305   CCcc 9536   RRcr 9537   0cc0 9538   1c1 9539   + caddc 9541   x. cmul 9543   +oocpnf 9671   < clt 9674   <_ cle 9675   - cmin 9859   / cdiv 10268   2c2 10659   RR+crp 11302   [,)cico 11637   Recre 13139   abscabs 13276   ↾_t crest 15278   TopOpenctopn 15279  ℂ_fldccnfld 18905   ^c ccxp 23370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-inf2 8146  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616  ax-addf 9617  ax-mulf 9618

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-se 4814  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-2o 7191  df-oadd 7194  df-er 7371  df-map 7482  df-pm 7483  df-ixp 7531  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-fsupp 7890  df-fi 7931  df-sup 7962  df-inf 7963  df-oi 8025  df-card 8372  df-cda 8596  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-fz 11783  df-fzo 11914  df-fl 12025  df-mod 12094  df-seq 12211  df-exp 12270  df-fac 12457  df-bc 12485  df-hash 12513  df-shft 13109  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-limsup 13504  df-clim 13530  df-rlim 13531  df-sum 13731  df-ef 14099  df-sin 14101  df-cos 14102  df-pi 14104  df-struct 15086  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-ress 15091  df-plusg 15165  df-mulr 15166  df-starv 15167  df-sca 15168  df-vsca 15169  df-ip 15170  df-tset 15171  df-ple 15172  df-ds 15174  df-unif 15175  df-hom 15176  df-cco 15177  df-rest 15280  df-topn 15281  df-0g 15299  df-gsum 15300  df-topgen 15301  df-pt 15302  df-prds 15305  df-xrs 15359  df-qtop 15364  df-imas 15365  df-xps 15367  df-mre 15443  df-mrc 15444  df-acs 15446  df-mgm 16439  df-sgrp 16478  df-mnd 16488  df-submnd 16534  df-mulg 16627  df-cntz 16922  df-cmn 17367  df-psmet 18897  df-xmet 18898  df-met 18899  df-bl 18900  df-mopn 18901  df-fbas 18902  df-fg 18903  df-cnfld 18906  df-top 19852  df-bases 19853  df-topon 19854  df-topsp 19855  df-cld 19965  df-ntr 19966  df-cls 19967  df-nei 20045  df-lp 20083  df-perf 20084  df-cn 20174  df-cnp 20175  df-haus 20262  df-tx 20508  df-hmeo 20701  df-fil 20792  df-fm 20884  df-flim 20885  df-flf 20886  df-xms 21266  df-ms 21267  df-tms 21268  df-cncf 21806  df-limc 22698  df-dv 22699  df-log 23371  df-cxp 23372

This theorem is referenced by:  cxpcn3  23553