Theorem cxpcn3lem 23099

Description: Lemma for cxpcn3 23100. (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 2521	. . . . . . . . . 10 |- ( A e. D <-> A e. ( `' Re " RR+ ) )
5		ref 12927	. . . . . . . . . . 11 |- Re : CC --> RR
6		ffn 5721	. . . . . . . . . . 11 |- ( Re : CC --> RR -> Re Fn CC )
7		elpreima 5992	. . . . . . . . . . 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 249	. . . . . . . . 9 |- ( A e. D <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) )
10	9	simprbi 464	. . . . . . . 8 |- ( A e. D -> ( Re ` A ) e. RR+ )
11	10	adantr 465	. . . . . . 7 |- ( ( A e. D /\ E e. RR+ ) -> ( Re ` A ) e. RR+ )
12		1rp 11235	. . . . . . 7 |- 1 e. RR+
13		ifcl 3968	. . . . . . 7 |- ( ( ( Re ` A ) e. RR+ /\ 1 e. RR+ ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
14	11, 12, 13	sylancl 662	. . . . . 6 |- ( ( A e. D /\ E e. RR+ ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
15	14	rphalfcld 11279	. . . . 5 |- ( ( A e. D /\ E e. RR+ ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) e. RR+ )
16	2, 15	syl5eqel 2535	. . . 4 |- ( ( A e. D /\ E e. RR+ ) -> U e. RR+ )
17		simpr 461	. . . . 5 |- ( ( A e. D /\ E e. RR+ ) -> E e. RR+ )
18	16	rpreccld 11277	. . . . . 6 |- ( ( A e. D /\ E e. RR+ ) -> ( 1 / U ) e. RR+ )
19	18	rpred 11267	. . . . 5 |- ( ( A e. D /\ E e. RR+ ) -> ( 1 / U ) e. RR )
20	17, 19	rpcxpcld 23089	. . . 4 |- ( ( A e. D /\ E e. RR+ ) -> ( E ^c ( 1 / U ) ) e. RR+ )
21	16, 20	ifcld 3969	. . 3 |- ( ( A e. D /\ E e. RR+ ) -> if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) e. RR+ )
22	1, 21	syl5eqel 2535	. 2 |- ( ( A e. D /\ E e. RR+ ) -> T e. RR+ )
23		elrege0 11638	. . . 4 |- ( a e. ( 0 [,) +oo ) <-> ( a e. RR /\ 0 <_ a ) )
24		0red 9600	. . . . . . 7 |- ( ( A e. D /\ E e. RR+ ) -> 0 e. RR )
25		leloe 9674	. . . . . . 7 |- ( ( 0 e. RR /\ a e. RR ) -> ( 0 <_ a <-> ( 0 < a \/ 0 = a ) ) )
26	24, 25	sylan 471	. . . . . 6 |- ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( 0 <_ a <-> ( 0 < a \/ 0 = a ) ) )
27		elrp 11233	. . . . . . . . 9 |- ( a e. RR+ <-> ( a e. RR /\ 0 < a ) )
28		simp2l 1023	. . . . . . . . . . . . . 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 1024	. . . . . . . . . . . . . . 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 5347	. . . . . . . . . . . . . . . . . 18 |- ( `' Re " RR+ ) C_ dom Re
31	5	fdmi 5726	. . . . . . . . . . . . . . . . . 18 |- dom Re = CC
32	30, 31	sseqtri 3521	. . . . . . . . . . . . . . . . 17 |- ( `' Re " RR+ ) C_ CC
33	3, 32	eqsstri 3519	. . . . . . . . . . . . . . . 16 |- D C_ CC
34	33	sseli 3485	. . . . . . . . . . . . . . 15 |- ( b e. D -> b e. CC )
35	29, 34	syl 16	. . . . . . . . . . . . . 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 23051	. . . . . . . . . . . . . 14 |- ( ( a e. RR+ /\ b e. CC ) -> ( abs ` ( a ^c b ) ) = ( a ^c ( Re ` b ) ) )
37	28, 35, 36	syl2anc 661	. . . . . . . . . . . . 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 13009	. . . . . . . . . . . . . . . 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 23089	. . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . 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 23089	. . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . 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 1022	. . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . 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 1021	. . . . . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . . . . . 19 |- ( A e. D -> A e. CC )
49	47, 48	syl 16	. . . . . . . . . . . . . . . . . 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 13009	. . . . . . . . . . . . . . . . 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 10792	. . . . . . . . . . . . . . . 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 9598	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
53		min1 11400	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ ( Re ` A ) )
54	50, 52, 53	sylancl 662	. . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . . . . 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 10612	. . . . . . . . . . . . . . . . . . . 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 10634	. . . . . . . . . . . . . . . . . . . 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 10414	. . . . . . . . . . . . . . . . . . 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 1233	. . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . 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 4470	. . . . . . . . . . . . . . . 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 9625	. . . . . . . . . . . . . . . . . . 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 10791	. . . . . . . . . . . . . . . . . 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 13031	. . . . . . . . . . . . . . . . . . . 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 9936	. . . . . . . . . . . . . . . . . . . . . 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 13009	. . . . . . . . . . . . . . . . . . . . 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 13249	. . . . . . . . . . . . . . . . . . . . . 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 13264	. . . . . . . . . . . . . . . . . . . . . 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 1026	. . . . . . . . . . . . . . . . . . . . . . . . 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 4476	. . . . . . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . . . . . . . . . . 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 11405	. . . . . . . . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . . . 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 9743	. . . . . . . . . . . . . . . . . . . . 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 9745	. . . . . . . . . . . . . . . . . . . 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 4459	. . . . . . . . . . . . . . . . . . 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 10157	. . . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . . 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 4457	. . . . . . . . . . . . . . . . 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 10152	. . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . 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 9743	. . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . . 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 11274	. . . . . . . . . . . . . . . . . . . . . 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 13111	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. RR /\ 0 <_ a ) -> ( abs ` a ) = a )
93	91, 92	syl 16	. . . . . . . . . . . . . . . . . . . . 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 1025	. . . . . . . . . . . . . . . . . . . . 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 4459	. . . . . . . . . . . . . . . . . . . 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 4476	. . . . . . . . . . . . . . . . . . 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 11405	. . . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < U )
101		rehalfcl 10772	. . . . . . . . . . . . . . . . . . 19 |- ( 1 e. RR -> ( 1 / 2 ) e. RR )
102	52, 101	mp1i 12	. . . . . . . . . . . . . . . . . 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 11401	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ 1 )
104	50, 52, 103	sylancl 662	. . . . . . . . . . . . . . . . . . . 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 10414	. . . . . . . . . . . . . . . . . . . . 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 1233	. . . . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . . . 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 4470	. . . . . . . . . . . . . . . . . 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 10764	. . . . . . . . . . . . . . . . . . 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 9743	. . . . . . . . . . . . . . . . 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 9746	. . . . . . . . . . . . . . . 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 23091	. . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . 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 11276	. . . . . . . . . . . . . . . . . . 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 10228	. . . . . . . . . . . . . . . . . . 19 |- ( ( U e. CC /\ U =/= 0 ) -> ( U x. ( 1 / U ) ) = 1 )
117	115, 116	syl 16	. . . . . . . . . . . . . . . . . 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 6297	. . . . . . . . . . . . . . . . 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 11277	. . . . . . . . . . . . . . . . . . 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 11269	. . . . . . . . . . . . . . . . . 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 23093	. . . . . . . . . . . . . . . . 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 11269	. . . . . . . . . . . . . . . . . 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 23065	. . . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 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 4457	. . . . . . . . . . . . . . 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 11274	. . . . . . . . . . . . . . . 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 11274	. . . . . . . . . . . . . . . 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 23057	. . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 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 9746	. . . . . . . . . . . . 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 4457	. . . . . . . . . . . 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 1199	. . . . . . . . . . 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 648	. . . . . . . . . 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 2857	. . . . . . . . 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 476	. . . . . . . 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 615	. . . . . . 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 5992	. . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . 17 |- ( b e. ( `' Re " RR+ ) -> ( Re ` b ) e. RR+ )
142	141, 3	eleq2s 2551	. . . . . . . . . . . . . . . 16 |- ( b e. D -> ( Re ` b ) e. RR+ )
143	142	rpne0d 11272	. . . . . . . . . . . . . . 15 |- ( b e. D -> ( Re ` b ) =/= 0 )
144		fveq2 5856	. . . . . . . . . . . . . . . . 17 |- ( b = 0 -> ( Re ` b ) = ( Re ` 0 ) )
145		re0 12967	. . . . . . . . . . . . . . . . 17 |- ( Re ` 0 ) = 0
146	144, 145	syl6eq 2500	. . . . . . . . . . . . . . . 16 |- ( b = 0 -> ( Re ` b ) = 0 )
147	146	necon3i 2683	. . . . . . . . . . . . . . 15 |- ( ( Re ` b ) =/= 0 -> b =/= 0 )
148	143, 147	syl 16	. . . . . . . . . . . . . 14 |- ( b e. D -> b =/= 0 )
149	34, 148	0cxpd 23069	. . . . . . . . . . . . 13 |- ( b e. D -> ( 0 ^c b ) = 0 )
150	149	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 ^c b ) = 0 )
151	150	abs00bd 13106	. . . . . . . . . . 11 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( abs ` ( 0 ^c b ) ) = 0 )
152		simpllr 760	. . . . . . . . . . . 12 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> E e. RR+ )
153	152	rpgt0d 11270	. . . . . . . . . . 11 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> 0 < E )
154	151, 153	eqbrtrd 4457	. . . . . . . . . 10 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( abs ` ( 0 ^c b ) ) < E )
155		oveq1 6288	. . . . . . . . . . . 12 |- ( 0 = a -> ( 0 ^c b ) = ( a ^c b ) )
156	155	fveq2d 5860	. . . . . . . . . . 11 |- ( 0 = a -> ( abs ` ( 0 ^c b ) ) = ( abs ` ( a ^c b ) ) )
157	156	breq1d 4447	. . . . . . . . . 10 |- ( 0 = a -> ( ( abs ` ( 0 ^c b ) ) < E <-> ( abs ` ( a ^c b ) ) < E ) )
158	154, 157	syl5ibcom 220	. . . . . . . . 9 |- ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 = a -> ( abs ` ( a ^c b ) ) < E ) )
159	158	a1dd 46	. . . . . . . 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 2861	. . . . . . 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 380	. . . . . 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 215	. . . . 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 603	. . . 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 217	. . 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 2855	. 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 4441	. . . . . 6 |- ( d = T -> ( ( abs ` a ) < d <-> ( abs ` a ) < T ) )
167		breq2 4441	. . . . . 6 |- ( d = T -> ( ( abs ` ( A - b ) ) < d <-> ( abs ` ( A - b ) ) < T ) )
168	166, 167	anbi12d 710	. . . . 5 |- ( d = T -> ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) <-> ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) )
169	168	imbi1d 317	. . . 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 2887	. . 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 3196	. 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 661	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 184   \/ wo 368   /\ wa 369   /\ w3a 974   = wceq 1383   e. wcel 1804   =/= wne 2638   A.wral 2793   E.wrex 2794   ifcif 3926   class class class wbr 4437   `'ccnv 4988   dom cdm 4989   "cima 4992   Fn wfn 5573   -->wf 5574   ` cfv 5578  (class class class)co 6281   CCcc 9493   RRcr 9494   0cc0 9495   1c1 9496   + caddc 9498   x. cmul 9500   +oocpnf 9628   < clt 9631   <_ cle 9632   - cmin 9810   / cdiv 10213   2c2 10592   RR+crp 11231   [,)cico 11542   Recre 12912   abscabs 13049   ↾_t crest 14800   TopOpenctopn 14801  ℂ_fldccnfld 18399   ^c ccxp 22921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-inf2 8061  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573  ax-addf 9574  ax-mulf 9575

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-fal 1389  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6904  df-recs 7044  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-ixp 7472  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-fsupp 7832  df-fi 7873  df-sup 7903  df-oi 7938  df-card 8323  df-cda 8551  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10214  df-nn 10544  df-2 10601  df-3 10602  df-4 10603  df-5 10604  df-6 10605  df-7 10606  df-8 10607  df-9 10608  df-10 10609  df-n0 10803  df-z 10872  df-dec 10987  df-uz 11093  df-q 11194  df-rp 11232  df-xneg 11329  df-xadd 11330  df-xmul 11331  df-ioo 11544  df-ioc 11545  df-ico 11546  df-icc 11547  df-fz 11684  df-fzo 11807  df-fl 11911  df-mod 11979  df-seq 12090  df-exp 12149  df-fac 12336  df-bc 12363  df-hash 12388  df-shft 12882  df-cj 12914  df-re 12915  df-im 12916  df-sqrt 13050  df-abs 13051  df-limsup 13276  df-clim 13293  df-rlim 13294  df-sum 13491  df-ef 13785  df-sin 13787  df-cos 13788  df-pi 13790  df-struct 14616  df-ndx 14617  df-slot 14618  df-base 14619  df-sets 14620  df-ress 14621  df-plusg 14692  df-mulr 14693  df-starv 14694  df-sca 14695  df-vsca 14696  df-ip 14697  df-tset 14698  df-ple 14699  df-ds 14701  df-unif 14702  df-hom 14703  df-cco 14704  df-rest 14802  df-topn 14803  df-0g 14821  df-gsum 14822  df-topgen 14823  df-pt 14824  df-prds 14827  df-xrs 14881  df-qtop 14886  df-imas 14887  df-xps 14889  df-mre 14965  df-mrc 14966  df-acs 14968  df-mgm 15851  df-sgrp 15890  df-mnd 15900  df-submnd 15946  df-mulg 16039  df-cntz 16334  df-cmn 16779  df-psmet 18390  df-xmet 18391  df-met 18392  df-bl 18393  df-mopn 18394  df-fbas 18395  df-fg 18396  df-cnfld 18400  df-top 19377  df-bases 19379  df-topon 19380  df-topsp 19381  df-cld 19498  df-ntr 19499  df-cls 19500  df-nei 19577  df-lp 19615  df-perf 19616  df-cn 19706  df-cnp 19707  df-haus 19794  df-tx 20041  df-hmeo 20234  df-fil 20325  df-fm 20417  df-flim 20418  df-flf 20419  df-xms 20801  df-ms 20802  df-tms 20803  df-cncf 21360  df-limc 22248  df-dv 22249  df-log 22922  df-cxp 22923

This theorem is referenced by:  cxpcn3  23100