Metamath Proof Explorer

Theorem cxpcn3lem

Description: Lemma for cxpcn3 . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses cxpcn3.d 
|- D = ( `' Re " RR+ )
cxpcn3.j 
|- J = ( TopOpen ` CCfld )
cxpcn3.k 
|- K = ( J |`t ( 0 [,) +oo ) )
cxpcn3.l 
|- L = ( J |`t D )
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 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 ) )

Proof

Step Hyp Ref Expression
1 cxpcn3.d 
 |-  D = ( `' Re " RR+ )
2 cxpcn3.j 
 |-  J = ( TopOpen ` CCfld )
3 cxpcn3.k 
 |-  K = ( J |`t ( 0 [,) +oo ) )
4 cxpcn3.l 
 |-  L = ( J |`t D )
5 cxpcn3.u 
 |-  U = ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 )
6 cxpcn3.t 
 |-  T = if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) )
7 1 eleq2i 
 |-  ( A e. D <-> A e. ( `' Re " RR+ ) )
8 ref 
 |-  Re : CC --> RR
9 ffn 
 |-  ( Re : CC --> RR -> Re Fn CC )
10 elpreima 
 |-  ( Re Fn CC -> ( A e. ( `' Re " RR+ ) <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) ) )
11 8 9 10 mp2b 
 |-  ( A e. ( `' Re " RR+ ) <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) )
12 7 11 bitri 
 |-  ( A e. D <-> ( A e. CC /\ ( Re ` A ) e. RR+ ) )
13 12 simprbi 
 |-  ( A e. D -> ( Re ` A ) e. RR+ )
14 13 adantr 
 |-  ( ( A e. D /\ E e. RR+ ) -> ( Re ` A ) e. RR+ )
15 1rp 
 |-  1 e. RR+
16 ifcl 
 |-  ( ( ( Re ` A ) e. RR+ /\ 1 e. RR+ ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
17 14 15 16 sylancl 
 |-  ( ( A e. D /\ E e. RR+ ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) e. RR+ )
18 17 rphalfcld 
 |-  ( ( A e. D /\ E e. RR+ ) -> ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 ) e. RR+ )
19 5 18 eqeltrid 
 |-  ( ( A e. D /\ E e. RR+ ) -> U e. RR+ )
20 simpr 
 |-  ( ( A e. D /\ E e. RR+ ) -> E e. RR+ )
21 19 rpreccld 
 |-  ( ( A e. D /\ E e. RR+ ) -> ( 1 / U ) e. RR+ )
22 21 rpred 
 |-  ( ( A e. D /\ E e. RR+ ) -> ( 1 / U ) e. RR )
23 20 22 rpcxpcld 
 |-  ( ( A e. D /\ E e. RR+ ) -> ( E ^c ( 1 / U ) ) e. RR+ )
24 19 23 ifcld 
 |-  ( ( A e. D /\ E e. RR+ ) -> if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) ) e. RR+ )
25 6 24 eqeltrid 
 |-  ( ( A e. D /\ E e. RR+ ) -> T e. RR+ )
26 elrege0 
 |-  ( a e. ( 0 [,) +oo ) <-> ( a e. RR /\ 0 <_ a ) )
27 0red 
 |-  ( ( A e. D /\ E e. RR+ ) -> 0 e. RR )
28 leloe 
 |-  ( ( 0 e. RR /\ a e. RR ) -> ( 0 <_ a <-> ( 0 < a \/ 0 = a ) ) )
29 27 28 sylan 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) -> ( 0 <_ a <-> ( 0 < a \/ 0 = a ) ) )
30 elrp 
 |-  ( a e. RR+ <-> ( a e. RR /\ 0 < a ) )
31 simp2l 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a e. RR+ )
32 simp2r 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> b e. D )
33 cnvimass 
 |-  ( `' Re " RR+ ) C_ dom Re
34 8 fdmi 
 |-  dom Re = CC
35 33 34 sseqtri 
 |-  ( `' Re " RR+ ) C_ CC
36 1 35 eqsstri 
 |-  D C_ CC
37 36 sseli 
 |-  ( b e. D -> b e. CC )
38 32 37 syl 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> b e. CC )
39 abscxp 
 |-  ( ( a e. RR+ /\ b e. CC ) -> ( abs ` ( a ^c b ) ) = ( a ^c ( Re ` b ) ) )
40 31 38 39 syl2anc 
 |-  ( ( ( 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 ) ) )
41 38 recld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` b ) e. RR )
42 31 41 rpcxpcld 
 |-  ( ( ( 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+ )
43 42 rpred 
 |-  ( ( ( 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 )
44 19 3ad2ant1 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U e. RR+ )
45 44 rpred 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U e. RR )
46 31 45 rpcxpcld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c U ) e. RR+ )
47 46 rpred 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c U ) e. RR )
48 simp1r 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> E e. RR+ )
49 48 rpred 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> E e. RR )
50 simp1l 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> A e. D )
51 12 simplbi 
 |-  ( A e. D -> A e. CC )
52 50 51 syl 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> A e. CC )
53 52 recld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` A ) e. RR )
54 53 rehalfcld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( Re ` A ) / 2 ) e. RR )
55 1re 
 |-  1 e. RR
56 min1 
 |-  ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ ( Re ` A ) )
57 53 55 56 sylancl 
 |-  ( ( ( 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 ) )
58 17 3ad2ant1 
 |-  ( ( ( 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+ )
59 58 rpred 
 |-  ( ( ( 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 )
60 2re 
 |-  2 e. RR
61 60 a1i 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> 2 e. RR )
62 2pos 
 |-  0 < 2
63 62 a1i 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> 0 < 2 )
64 lediv1 
 |-  ( ( 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 ) ) )
65 59 53 61 63 64 syl112anc 
 |-  ( ( ( 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 ) ) )
66 57 65 mpbid 
 |-  ( ( ( 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 ) )
67 5 66 eqbrtrid 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U <_ ( ( Re ` A ) / 2 ) )
68 53 recnd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` A ) e. CC )
69 68 2halvesd 
 |-  ( ( ( 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 ) )
70 52 38 resubd 
 |-  ( ( ( 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 ) ) )
71 52 38 subcld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( A - b ) e. CC )
72 71 recld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) e. RR )
73 71 abscld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) e. RR )
74 71 releabsd 
 |-  ( ( ( 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 ) ) )
75 simp3r 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) < T )
76 75 6 breqtrdi 
 |-  ( ( ( 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 ) ) ) )
77 23 3ad2ant1 
 |-  ( ( ( 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+ )
78 77 rpred 
 |-  ( ( ( 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 )
79 ltmin 
 |-  ( ( ( 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 ) ) ) ) )
80 73 45 78 79 syl3anc 
 |-  ( ( ( 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 ) ) ) ) )
81 76 80 mpbid 
 |-  ( ( ( 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 ) ) ) )
82 81 simpld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( A - b ) ) < U )
83 72 73 45 74 82 lelttrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( Re ` ( A - b ) ) < U )
84 72 45 54 83 67 ltletrd 
 |-  ( ( ( 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 ) )
85 70 84 eqbrtrrd 
 |-  ( ( ( 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 ) )
86 53 41 54 ltsubadd2d 
 |-  ( ( ( 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 ) ) ) )
87 85 86 mpbid 
 |-  ( ( ( 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 ) ) )
88 69 87 eqbrtrd 
 |-  ( ( ( 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 ) ) )
89 54 41 54 ltadd1d 
 |-  ( ( ( 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 ) ) ) )
90 88 89 mpbird 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( ( Re ` A ) / 2 ) < ( Re ` b ) )
91 45 54 41 67 90 lelttrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U < ( Re ` b ) )
92 31 rpred 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a e. RR )
93 55 a1i 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> 1 e. RR )
94 31 rprege0d 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a e. RR /\ 0 <_ a ) )
95 absid 
 |-  ( ( a e. RR /\ 0 <_ a ) -> ( abs ` a ) = a )
96 94 95 syl 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` a ) = a )
97 simp3l 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` a ) < T )
98 96 97 eqbrtrrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < T )
99 98 6 breqtrdi 
 |-  ( ( ( 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 ) ) ) )
100 ltmin 
 |-  ( ( 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 ) ) ) ) )
101 92 45 78 100 syl3anc 
 |-  ( ( ( 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 ) ) ) ) )
102 99 101 mpbid 
 |-  ( ( ( 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 ) ) ) )
103 102 simpld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < U )
104 rehalfcl 
 |-  ( 1 e. RR -> ( 1 / 2 ) e. RR )
105 55 104 mp1i 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / 2 ) e. RR )
106 min2 
 |-  ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) <_ 1 )
107 53 55 106 sylancl 
 |-  ( ( ( 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 )
108 lediv1 
 |-  ( ( 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 ) ) )
109 59 93 61 63 108 syl112anc 
 |-  ( ( ( 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 ) ) )
110 107 109 mpbid 
 |-  ( ( ( 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 ) )
111 5 110 eqbrtrid 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U <_ ( 1 / 2 ) )
112 halflt1 
 |-  ( 1 / 2 ) < 1
113 112 a1i 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / 2 ) < 1 )
114 45 105 93 111 113 lelttrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> U < 1 )
115 92 45 93 103 114 lttrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < 1 )
116 31 45 115 41 cxplt3d 
 |-  ( ( ( 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 ) ) )
117 91 116 mpbid 
 |-  ( ( ( 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 ) )
118 44 rpcnne0d 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( U e. CC /\ U =/= 0 ) )
119 recid 
 |-  ( ( U e. CC /\ U =/= 0 ) -> ( U x. ( 1 / U ) ) = 1 )
120 118 119 syl 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( U x. ( 1 / U ) ) = 1 )
121 120 oveq2d 
 |-  ( ( ( 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 ) )
122 44 rpreccld 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / U ) e. RR+ )
123 122 rpcnd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( 1 / U ) e. CC )
124 31 45 123 cxpmuld 
 |-  ( ( ( 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 ) ) )
125 31 rpcnd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a e. CC )
126 125 cxp1d 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c 1 ) = a )
127 121 124 126 3eqtr3d 
 |-  ( ( ( 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 )
128 102 simprd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> a < ( E ^c ( 1 / U ) ) )
129 127 128 eqbrtrd 
 |-  ( ( ( 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 ) ) )
130 46 rprege0d 
 |-  ( ( ( 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 ) ) )
131 48 rprege0d 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( E e. RR /\ 0 <_ E ) )
132 cxplt2 
 |-  ( ( ( ( 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 ) ) ) )
133 130 131 122 132 syl3anc 
 |-  ( ( ( 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 ) ) ) )
134 129 133 mpbird 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c U ) < E )
135 43 47 49 117 134 lttrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( a ^c ( Re ` b ) ) < E )
136 40 135 eqbrtrd 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) /\ ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) -> ( abs ` ( a ^c b ) ) < E )
137 136 3expia 
 |-  ( ( ( A e. D /\ E e. RR+ ) /\ ( a e. RR+ /\ b e. D ) ) -> ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
138 137 anassrs 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR+ ) /\ b e. D ) -> ( ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) -> ( abs ` ( a ^c b ) ) < E ) )
139 138 ralrimiva 
 |-  ( ( ( 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 ) )
140 30 139 sylan2br 
 |-  ( ( ( 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 ) )
141 140 expr 
 |-  ( ( ( 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 ) ) )
142 elpreima 
 |-  ( Re Fn CC -> ( b e. ( `' Re " RR+ ) <-> ( b e. CC /\ ( Re ` b ) e. RR+ ) ) )
143 8 9 142 mp2b 
 |-  ( b e. ( `' Re " RR+ ) <-> ( b e. CC /\ ( Re ` b ) e. RR+ ) )
144 143 simprbi 
 |-  ( b e. ( `' Re " RR+ ) -> ( Re ` b ) e. RR+ )
145 144 1 eleq2s 
 |-  ( b e. D -> ( Re ` b ) e. RR+ )
146 145 rpne0d 
 |-  ( b e. D -> ( Re ` b ) =/= 0 )
147 fveq2 
 |-  ( b = 0 -> ( Re ` b ) = ( Re ` 0 ) )
148 re0 
 |-  ( Re ` 0 ) = 0
149 147 148 eqtrdi 
 |-  ( b = 0 -> ( Re ` b ) = 0 )
150 149 necon3i 
 |-  ( ( Re ` b ) =/= 0 -> b =/= 0 )
151 146 150 syl 
 |-  ( b e. D -> b =/= 0 )
152 37 151 0cxpd 
 |-  ( b e. D -> ( 0 ^c b ) = 0 )
153 152 adantl 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 ^c b ) = 0 )
154 153 abs00bd 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( abs ` ( 0 ^c b ) ) = 0 )
155 simpllr 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> E e. RR+ )
156 155 rpgt0d 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> 0 < E )
157 154 156 eqbrtrd 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( abs ` ( 0 ^c b ) ) < E )
158 fvoveq1 
 |-  ( 0 = a -> ( abs ` ( 0 ^c b ) ) = ( abs ` ( a ^c b ) ) )
159 158 breq1d 
 |-  ( 0 = a -> ( ( abs ` ( 0 ^c b ) ) < E <-> ( abs ` ( a ^c b ) ) < E ) )
160 157 159 syl5ibcom 
 |-  ( ( ( ( A e. D /\ E e. RR+ ) /\ a e. RR ) /\ b e. D ) -> ( 0 = a -> ( abs ` ( a ^c b ) ) < E ) )
161 160 a1dd 
 |-  ( ( ( ( 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 ) ) )
162 161 ralrimdva 
 |-  ( ( ( 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 141 162 jaod 
 |-  ( ( ( 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 ) ) )
164 29 163 sylbid 
 |-  ( ( ( 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 ) ) )
165 164 expimpd 
 |-  ( ( 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 ) ) )
166 26 165 syl5bi 
 |-  ( ( 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 ) ) )
167 166 ralrimiv 
 |-  ( ( 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 ) )
168 breq2 
 |-  ( d = T -> ( ( abs ` a ) < d <-> ( abs ` a ) < T ) )
169 breq2 
 |-  ( d = T -> ( ( abs ` ( A - b ) ) < d <-> ( abs ` ( A - b ) ) < T ) )
170 168 169 anbi12d 
 |-  ( d = T -> ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) <-> ( ( abs ` a ) < T /\ ( abs ` ( A - b ) ) < T ) ) )
171 170 imbi1d 
 |-  ( 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 ) ) )
172 171 2ralbidv 
 |-  ( 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 ) ) )
173 172 rspcev 
 |-  ( ( 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 ) )
174 25 167 173 syl2anc 
 |-  ( ( 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 ) )