Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cntotbnd Unicode version

Theorem cntotbnd 26395
Description: A subset of the complexes is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
Hypothesis
Ref Expression
cntotbnd.d  |-  D  =  ( ( abs  o.  -  )  |`  ( X  X.  X ) )
Assertion
Ref Expression
cntotbnd  |-  ( D  e.  ( TotBnd `  X
)  <->  D  e.  ( Bnd `  X ) )

Proof of Theorem cntotbnd
Dummy variables  a 
b  d  r  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 totbndbnd 26388 . 2  |-  ( D  e.  ( TotBnd `  X
)  ->  D  e.  ( Bnd `  X ) )
2 rpcn 10576 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  r  e.  CC )
32adantl 453 . . . . . . . . 9  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  r  e.  CC )
4 gzcn 13255 . . . . . . . . 9  |-  ( z  e.  ZZ [ _i ]  ->  z  e.  CC )
5 mulcl 9030 . . . . . . . . 9  |-  ( ( r  e.  CC  /\  z  e.  CC )  ->  ( r  x.  z
)  e.  CC )
63, 4, 5syl2an 464 . . . . . . . 8  |-  ( ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  /\  z  e.  ZZ [ _i ] )  -> 
( r  x.  z
)  e.  CC )
7 eqid 2404 . . . . . . . 8  |-  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  =  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )
86, 7fmptd 5852 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  (
z  e.  ZZ [
_i ]  |->  ( r  x.  z ) ) : ZZ [ _i ]
--> CC )
9 frn 5556 . . . . . . 7  |-  ( ( z  e.  ZZ [
_i ]  |->  ( r  x.  z ) ) : ZZ [ _i ]
--> CC  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  C_  CC )
108, 9syl 16 . . . . . 6  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) ) 
C_  CC )
11 cnex 9027 . . . . . . 7  |-  CC  e.  _V
1211elpw2 4324 . . . . . 6  |-  ( ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  e.  ~P CC  <->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  C_  CC )
1310, 12sylibr 204 . . . . 5  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  e.  ~P CC )
14 cnmet 18759 . . . . . . . . . . . . . . . . 17  |-  ( abs 
o.  -  )  e.  ( Met `  CC )
15 cntotbnd.d . . . . . . . . . . . . . . . . . 18  |-  D  =  ( ( abs  o.  -  )  |`  ( X  X.  X ) )
1615bnd2lem 26390 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs  o.  -  )  e.  ( Met `  CC )  /\  D  e.  ( Bnd `  X
) )  ->  X  C_  CC )
1714, 16mpan 652 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( Bnd `  X
)  ->  X  C_  CC )
1817sselda 3308 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  y  e.  X )  ->  y  e.  CC )
1918adantrl 697 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
y  e.  CC )
2019recld 11954 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Re `  y
)  e.  RR )
21 simprl 733 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR+ )
2220, 21rerpdivcld 10631 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  y )  /  r
)  e.  RR )
23 1re 9046 . . . . . . . . . . . . 13  |-  1  e.  RR
2423rehalfcli 10172 . . . . . . . . . . . 12  |-  ( 1  /  2 )  e.  RR
25 readdcl 9029 . . . . . . . . . . . 12  |-  ( ( ( ( Re `  y )  /  r
)  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) )  e.  RR )
2622, 24, 25sylancl 644 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) )  e.  RR )
2726flcld 11162 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ )
2819imcld 11955 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Im `  y
)  e.  RR )
2928, 21rerpdivcld 10631 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Im `  y )  /  r
)  e.  RR )
30 readdcl 9029 . . . . . . . . . . . 12  |-  ( ( ( ( Im `  y )  /  r
)  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) )  e.  RR )
3129, 24, 30sylancl 644 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) )  e.  RR )
3231flcld 11162 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ )
33 gzreim 13262 . . . . . . . . . 10  |-  ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ  /\  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  e.  ZZ )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  e.  ZZ [
_i ] )
3427, 32, 33syl2anc 643 . . . . . . . . 9  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  e.  ZZ [
_i ] )
35 gzcn 13255 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) )  e.  ZZ [ _i ]  ->  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  e.  CC )
3634, 35syl 16 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  e.  CC )
3721rpcnd 10606 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  CC )
3821rpne0d 10609 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  =/=  0 )
3919, 37, 38divcld 9746 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  e.  CC )
4036, 39subcld 9367 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) )  e.  CC )
4140abscld 12193 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) )  e.  RR )
4223a1i 11 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
1  e.  RR )
4327zcnd 10332 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  CC )
44 ax-icn 9005 . . . . . . . . . . . . . . . . . . . . 21  |-  _i  e.  CC
4532zcnd 10332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  CC )
46 mulcl 9030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( _i  e.  CC  /\  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  e.  CC )  -> 
( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  e.  CC )
4744, 45, 46sylancr 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  e.  CC )
4822recnd 9070 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  y )  /  r
)  e.  CC )
4929recnd 9070 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Im `  y )  /  r
)  e.  CC )
50 mulcl 9030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( _i  e.  CC  /\  ( ( Im `  y )  /  r
)  e.  CC )  ->  ( _i  x.  ( ( Im `  y )  /  r
) )  e.  CC )
5144, 49, 50sylancr 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
( Im `  y
)  /  r ) )  e.  CC )
5243, 47, 48, 51addsub4d 9414 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( ( ( Re `  y
)  /  r )  +  ( _i  x.  ( ( Im `  y )  /  r
) ) ) )  =  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Re
`  y )  / 
r ) )  +  ( ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) )  -  ( _i  x.  ( ( Im
`  y )  / 
r ) ) ) ) )
5339replimd 11957 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  =  ( ( Re `  ( y  /  r ) )  +  ( _i  x.  ( Im `  ( y  /  r ) ) ) ) )
5421rpred 10604 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR )
5554, 19, 38redivd 11989 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Re `  (
y  /  r ) )  =  ( ( Re `  y )  /  r ) )
5654, 19, 38imdivd 11990 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Im `  (
y  /  r ) )  =  ( ( Im `  y )  /  r ) )
5756oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
Im `  ( y  /  r ) ) )  =  ( _i  x.  ( ( Im
`  y )  / 
r ) ) )
5855, 57oveq12d 6058 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  ( y  /  r
) )  +  ( _i  x.  ( Im
`  ( y  / 
r ) ) ) )  =  ( ( ( Re `  y
)  /  r )  +  ( _i  x.  ( ( Im `  y )  /  r
) ) ) )
5953, 58eqtrd 2436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  =  ( ( ( Re `  y
)  /  r )  +  ( _i  x.  ( ( Im `  y )  /  r
) ) ) )
6059oveq2d 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) )  =  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) )  -  (
( ( Re `  y )  /  r
)  +  ( _i  x.  ( ( Im
`  y )  / 
r ) ) ) ) )
6144a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  ->  _i  e.  CC )
6261, 45, 49subdid 9445 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  =  ( ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  -  ( _i  x.  ( ( Im `  y )  /  r
) ) ) )
6362oveq2d 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) )  +  ( _i  x.  ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ) )  =  ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) )  +  ( ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) )  -  ( _i  x.  (
( Im `  y
)  /  r ) ) ) ) )
6452, 60, 633eqtr4d 2446 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) )  =  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Re
`  y )  / 
r ) )  +  ( _i  x.  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) ) ) )
6564fveq2d 5691 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) )  =  ( abs `  ( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) )  +  ( _i  x.  ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ) ) ) )
6665oveq1d 6055 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ^ 2 )  =  ( ( abs `  ( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) )  +  ( _i  x.  ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ) ) ) ^ 2 ) )
6727zred 10331 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  RR )
6867, 22resubcld 9421 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  RR )
6932zred 10331 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  RR )
7069, 29resubcld 9421 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  RR )
71 absreimsq 12052 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  RR  /\  ( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  RR )  ->  ( ( abs `  ( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) )  +  ( _i  x.  ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ) ) ) ^ 2 )  =  ( ( ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) ) ^ 2 )  +  ( ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ^
2 ) ) )
7268, 70, 71syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  +  ( _i  x.  ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ) ) ) ^ 2 )  =  ( ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) ^ 2 )  +  ( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 ) ) )
7366, 72eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ^ 2 )  =  ( ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) ^ 2 )  +  ( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 ) ) )
7468resqcld 11504 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  e.  RR )
7570resqcld 11504 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  e.  RR )
7624resqcli 11422 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  /  2 ) ^ 2 )  e.  RR
7776a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( 1  / 
2 ) ^ 2 )  e.  RR )
7824a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( 1  /  2
)  e.  RR )
79 absresq 12062 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) )  e.  RR  ->  (
( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) ) ^ 2 )  =  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Re
`  y )  / 
r ) ) ^
2 ) )
8068, 79syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) ) ^ 2 )  =  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Re
`  y )  / 
r ) ) ^
2 ) )
81 rddif 12099 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Re `  y
)  /  r )  e.  RR  ->  ( abs `  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) )  <_ 
( 1  /  2
) )
8222, 81syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) )  <_  ( 1  /  2 ) )
8368recnd 9070 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  CC )
8483abscld 12193 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) )  e.  RR )
8583absge0d 12201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( abs `  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) ) ) )
86 halfgt0 10144 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  ( 1  /  2
)
8724, 86elrpii 10571 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  e.  RR+
88 rpge0 10580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  /  2 )  e.  RR+  ->  0  <_ 
( 1  /  2
) )
8987, 88mp1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( 1  /  2 ) )
9084, 78, 85, 89le2sqd 11513 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) )  <_  ( 1  /  2 )  <->  ( ( abs `  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ) ^
2 )  <_  (
( 1  /  2
) ^ 2 ) ) )
9182, 90mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) ) ^ 2 )  <_  ( ( 1  /  2 ) ^
2 ) )
9280, 91eqbrtrrd 4194 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  <_  ( (
1  /  2 ) ^ 2 ) )
9324recni 9058 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  2 )  e.  CC
9493sqvali 11416 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 ) ^ 2 )  =  ( ( 1  / 
2 )  x.  (
1  /  2 ) )
95 halflt1 10145 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  <  1
9624, 23, 24, 86ltmul1ii 9895 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  /  2 )  <  1  <->  ( (
1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  x.  (
1  /  2 ) ) )
9795, 96mpbi 200 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  x.  (
1  /  2 ) )
9893mulid2i 9049 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  x.  ( 1  / 
2 ) )  =  ( 1  /  2
)
9997, 98breqtri 4195 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  /  2
)
10094, 99eqbrtri 4191 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  /  2 ) ^ 2 )  < 
( 1  /  2
)
101100a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( 1  / 
2 ) ^ 2 )  <  ( 1  /  2 ) )
10274, 77, 78, 92, 101lelttrd 9184 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  <  ( 1  /  2 ) )
103 absresq 12062 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) )  e.  RR  ->  (
( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) ) ^ 2 )  =  ( ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ^
2 ) )
10470, 103syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) ) ^ 2 )  =  ( ( ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Im
`  y )  / 
r ) ) ^
2 ) )
105 rddif 12099 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Im `  y
)  /  r )  e.  RR  ->  ( abs `  ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) )  <_ 
( 1  /  2
) )
10629, 105syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  <_  ( 1  /  2 ) )
10770recnd 9070 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  CC )
108107abscld 12193 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  e.  RR )
109107absge0d 12201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( abs `  ( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) ) ) )
110108, 78, 109, 89le2sqd 11513 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  <_  ( 1  /  2 )  <->  ( ( abs `  ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ) ^
2 )  <_  (
( 1  /  2
) ^ 2 ) ) )
111106, 110mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) ) ^ 2 )  <_  ( ( 1  /  2 ) ^
2 ) )
112104, 111eqbrtrrd 4194 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  <_  ( (
1  /  2 ) ^ 2 ) )
11375, 77, 78, 112, 101lelttrd 9184 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  <  ( 1  /  2 ) )
11474, 75, 42, 102, 113lt2halvesd 10171 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  -  ( ( Re
`  y )  / 
r ) ) ^
2 )  +  ( ( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) ) ^ 2 ) )  <  1 )
11573, 114eqbrtrd 4192 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ^ 2 )  <  1 )
116 sq1 11431 . . . . . . . . . . . . . 14  |-  ( 1 ^ 2 )  =  1
117115, 116syl6breqr 4212 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ^ 2 )  <  ( 1 ^ 2 ) )
11840absge0d 12201 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( abs `  ( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) )
119 0le1 9507 . . . . . . . . . . . . . . 15  |-  0  <_  1
120119a1i 11 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  1 )
12141, 42, 118, 120lt2sqd 11512 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) )  <  1  <->  (
( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ^ 2 )  <  ( 1 ^ 2 ) ) )
122117, 121mpbird 224 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) )  <  1 )
12341, 42, 21, 122ltmul2dd 10656 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  ( abs `  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) )  -  (
y  /  r ) ) ) )  < 
( r  x.  1 ) )
12437, 36mulcld 9064 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) ) )  e.  CC )
125 eqid 2404 . . . . . . . . . . . . . 14  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
126125cnmetdval 18758 . . . . . . . . . . . . 13  |-  ( ( ( r  x.  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) ) )  e.  CC  /\  y  e.  CC )  ->  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( abs 
o.  -  ) y
)  =  ( abs `  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) )  -  y
) ) )
127124, 19, 126syl2anc 643 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( abs 
o.  -  ) y
)  =  ( abs `  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) )  -  y
) ) )
12837, 36, 39subdid 9445 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) )  =  ( ( r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) )  -  ( r  x.  (
y  /  r ) ) ) )
12919, 37, 38divcan2d 9748 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  (
y  /  r ) )  =  y )
130129oveq2d 6056 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) )  -  (
r  x.  ( y  /  r ) ) )  =  ( ( r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) )  -  y ) )
131128, 130eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) )  =  ( ( r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) )  -  y ) )
132131fveq2d 5691 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
r  x.  ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) )  -  ( y  / 
r ) ) ) )  =  ( abs `  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) )  -  y
) ) )
13337, 40absmuld 12211 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
r  x.  ( ( ( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) )  -  ( y  / 
r ) ) ) )  =  ( ( abs `  r )  x.  ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ) )
134132, 133eqtr3d 2438 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( r  x.  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) ) )  -  y ) )  =  ( ( abs `  r )  x.  ( abs `  (
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ) )
13521rpge0d 10608 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  r )
13654, 135absidd 12180 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  r
)  =  r )
137136oveq1d 6055 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  r
)  x.  ( abs `  ( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) )  =  ( r  x.  ( abs `  ( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  -  ( y  /  r ) ) ) ) )
138127, 134, 1373eqtrrd 2441 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  ( abs `  ( ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) )  -  (
y  /  r ) ) ) )  =  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( abs 
o.  -  ) y
) )
13937mulid1d 9061 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  1 )  =  r )
140123, 138, 1393brtr3d 4201 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( abs 
o.  -  ) y
)  <  r )
141 cnxmet 18760 . . . . . . . . . . . 12  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
142141a1i 11 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs  o.  -  )  e.  ( * Met `  CC ) )
143 rpxr 10575 . . . . . . . . . . . 12  |-  ( r  e.  RR+  ->  r  e. 
RR* )
144143ad2antrl 709 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR* )
145 elbl2 18373 . . . . . . . . . . 11  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  r  e.  RR* )  /\  ( ( r  x.  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) )  e.  CC  /\  y  e.  CC ) )  ->  ( y  e.  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( ball `  ( abs  o.  -  ) ) r )  <-> 
( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( abs 
o.  -  ) y
)  <  r )
)
146142, 144, 124, 19, 145syl22anc 1185 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  e.  ( ( r  x.  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) ) ) ( ball `  ( abs  o.  -  ) ) r )  <->  ( (
r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) ) ( abs  o.  -  )
y )  <  r
) )
147140, 146mpbird 224 . . . . . . . . 9  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
y  e.  ( ( r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) ) (
ball `  ( abs  o. 
-  ) ) r ) )
148 oveq2 6048 . . . . . . . . . . . 12  |-  ( z  =  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  ->  ( r  x.  z )  =  ( r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) ) )
149148oveq1d 6055 . . . . . . . . . . 11  |-  ( z  =  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  ->  ( (
r  x.  z ) ( ball `  ( abs  o.  -  ) ) r )  =  ( ( r  x.  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) ) ) ) ) ( ball `  ( abs  o.  -  ) ) r ) )
150149eleq2d 2471 . . . . . . . . . 10  |-  ( z  =  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  ->  ( y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r )  <-> 
y  e.  ( ( r  x.  ( ( |_ `  ( ( ( Re `  y
)  /  r )  +  ( 1  / 
2 ) ) )  +  ( _i  x.  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) ) ) ) ) (
ball `  ( abs  o. 
-  ) ) r ) ) )
151150rspcev 3012 . . . . . . . . 9  |-  ( ( ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) )  e.  ZZ [
_i ]  /\  y  e.  ( ( r  x.  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  +  ( _i  x.  ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) ) ) ) ( ball `  ( abs  o.  -  ) ) r ) )  ->  E. z  e.  ZZ [ _i ] 
y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) )
15234, 147, 151syl2anc 643 . . . . . . . 8  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  ->  E. z  e.  ZZ [ _i ]  y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) )
153152expr 599 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  (
y  e.  X  ->  E. z  e.  ZZ [ _i ]  y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) ) )
154 eliun 4057 . . . . . . . 8  |-  ( y  e.  U_ x  e. 
ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z
) ) ( x ( ball `  ( abs  o.  -  ) ) r )  <->  E. x  e.  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z
) ) y  e.  ( x ( ball `  ( abs  o.  -  ) ) r ) )
155 ovex 6065 . . . . . . . . . 10  |-  ( r  x.  z )  e. 
_V
156155rgenw 2733 . . . . . . . . 9  |-  A. z  e.  ZZ [ _i ] 
( r  x.  z
)  e.  _V
157 oveq1 6047 . . . . . . . . . . 11  |-  ( x  =  ( r  x.  z )  ->  (
x ( ball `  ( abs  o.  -  ) ) r )  =  ( ( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r ) )
158157eleq2d 2471 . . . . . . . . . 10  |-  ( x  =  ( r  x.  z )  ->  (
y  e.  ( x ( ball `  ( abs  o.  -  ) ) r )  <->  y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) ) )
1597, 158rexrnmpt 5838 . . . . . . . . 9  |-  ( A. z  e.  ZZ [ _i ]  ( r  x.  z )  e.  _V  ->  ( E. x  e. 
ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z
) ) y  e.  ( x ( ball `  ( abs  o.  -  ) ) r )  <->  E. z  e.  ZZ [ _i ]  y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) ) )
160156, 159ax-mp 8 . . . . . . . 8  |-  ( E. x  e.  ran  (
z  e.  ZZ [
_i ]  |->  ( r  x.  z ) ) y  e.  ( x ( ball `  ( abs  o.  -  ) ) r )  <->  E. z  e.  ZZ [ _i ] 
y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) )
161154, 160bitri 241 . . . . . . 7  |-  ( y  e.  U_ x  e. 
ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z
) ) ( x ( ball `  ( abs  o.  -  ) ) r )  <->  E. z  e.  ZZ [ _i ] 
y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) )
162153, 161syl6ibr 219 . . . . . 6  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  (
y  e.  X  -> 
y  e.  U_ x  e.  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z
) ) ( x ( ball `  ( abs  o.  -  ) ) r ) ) )
163162ssrdv 3314 . . . . 5  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  X  C_ 
U_ x  e.  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) ) ( x ( ball `  ( abs  o.  -  ) ) r ) )
164 simpl 444 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  D  e.  ( Bnd `  X
) )
165 0cn 9040 . . . . . . . 8  |-  0  e.  CC
16615ssbnd 26387 . . . . . . . 8  |-  ( ( ( abs  o.  -  )  e.  ( Met `  CC )  /\  0  e.  CC )  ->  ( D  e.  ( Bnd `  X )  <->  E. d  e.  RR  X  C_  (
0 ( ball `  ( abs  o.  -  ) ) d ) ) )
16714, 165, 166mp2an 654 . . . . . . 7  |-  ( D  e.  ( Bnd `  X
)  <->  E. d  e.  RR  X  C_  ( 0 (
ball `  ( abs  o. 
-  ) ) d ) )
168164, 167sylib 189 . . . . . 6  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  E. d  e.  RR  X  C_  (
0 ( ball `  ( abs  o.  -  ) ) d ) )
169 fzfi 11266 . . . . . . . . 9  |-  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) )  e.  Fin
170 xpfi 7337 . . . . . . . . 9  |-  ( ( ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) )  e.  Fin  /\  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) )  e.  Fin )  ->  ( ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ) )  e.  Fin )
171169, 169, 170mp2an 654 . . . . . . . 8  |-  ( (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) )  e.  Fin
172 eqid 2404 . . . . . . . . . 10  |-  ( a  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ) ,  b  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) 
|->  ( r  x.  (
a  +  ( _i  x.  b ) ) ) )  =  ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) ,  b  e.  (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) )
173 ovex 6065 . . . . . . . . . 10  |-  ( r  x.  ( a  +  ( _i  x.  b
) ) )  e. 
_V
174172, 173fnmpt2i 6379 . . . . . . . . 9  |-  ( a  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ) ,  b  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) 
|->  ( r  x.  (
a  +  ( _i  x.  b ) ) ) )  Fn  (
( -u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) )
175 dffn4 5618 . . . . . . . . 9  |-  ( ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) ,  b  e.  (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) )  Fn  ( ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) )  <->  ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) ,  b  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) ) : ( (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) ) -onto-> ran  ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) ,  b  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) ) )
176174, 175mpbi 200 . . . . . . . 8  |-  ( a  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ) ,  b  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) 
|->  ( r  x.  (
a  +  ( _i  x.  b ) ) ) ) : ( ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) ) -onto-> ran  ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) ,  b  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) )
177 fofi 7351 . . . . . . . 8  |-  ( ( ( ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) )  e. 
Fin  /\  ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) ,  b  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) ) : ( (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) ) -onto-> ran  ( a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ) ,  b  e.  ( -u (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ... ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) ) )  ->  ran  ( a  e.  (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) ) ,  b  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b
) ) ) )  e.  Fin )
178171, 176, 177mp2an 654 . . . . . . 7  |-  ran  (
a  e.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) ,  b  e.  (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  |->  ( r  x.  ( a  +  ( _i  x.  b ) ) ) )  e. 
Fin
1797, 155elrnmpti 5080 . . . . . . . . . 10  |-  ( x  e.  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  <->  E. z  e.  ZZ [ _i ]  x  =  ( r  x.  z ) )
180 elgz 13254 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  ZZ [ _i ] 
<->  ( z  e.  CC  /\  ( Re `  z
)  e.  ZZ  /\  ( Im `  z )  e.  ZZ ) )
181180simp2bi 973 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ZZ [ _i ]  ->  ( Re `  z )  e.  ZZ )
182181ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( Re `  z
)  e.  ZZ )
183182zcnd 10332 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( Re `  z
)  e.  CC )
184183abscld 12193 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  (
Re `  z )
)  e.  RR )
1854ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
z  e.  CC )
186185abscld 12193 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  z
)  e.  RR )
187 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  r  e.  RR+ )
188187adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
r  e.  RR+ )
189188rpred 10604 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
r  e.  RR )
190 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  d  e.  RR )
191190adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
d  e.  RR )
192189, 191readdcld 9071 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( r  +  d )  e.  RR )
193192, 188rerpdivcld 10631 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( r  +  d )  /  r
)  e.  RR )
194193flcld 11162 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( |_ `  (
( r  +  d )  /  r ) )  e.  ZZ )
195194peano2zd 10334 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 )  e.  ZZ )
196195zred 10331 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 )  e.  RR )
197 absrele 12068 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  CC  ->  ( abs `  ( Re `  z ) )  <_ 
( abs `  z
) )
198185, 197syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  (
Re `  z )
)  <_  ( abs `  z ) )
199188rpcnd 10606 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
r  e.  CC )
200199, 185absmuld 12211 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  (
r  x.  z ) )  =  ( ( abs `  r )  x.  ( abs `  z
) ) )
201188rpge0d 10608 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
0  <_  r )
202189, 201absidd 12180 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  r
)  =  r )
203202oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( abs `  r
)  x.  ( abs `  z ) )  =  ( r  x.  ( abs `  z ) ) )
204200, 203eqtrd 2436 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  (
r  x.  z ) )  =  ( r  x.  ( abs `  z
) ) )
205 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  X  C_  (
0 ( ball `  ( abs  o.  -  ) ) d ) )
206 sslin 3527 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( X 
C_  ( 0 (
ball `  ( abs  o. 
-  ) ) d )  ->  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  C_  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  (
0 ( ball `  ( abs  o.  -  ) ) d ) ) )
207205, 206syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  C_  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  (
0 ( ball `  ( abs  o.  -  ) ) d ) ) )
208141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  ( abs  o. 
-  )  e.  ( * Met `  CC ) )
2096adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  ( r  x.  z )  e.  CC )
210165a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  0  e.  CC )
211187rpxrd 10605 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  r  e.  RR* )
212190rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  d  e.  RR* )
213 bldisj 18381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  ( r  x.  z )  e.  CC  /\  0  e.  CC )  /\  ( r  e. 
RR*  /\  d  e.  RR* 
/\  ( r + e d )  <_ 
( ( r  x.  z ) ( abs 
o.  -  ) 0 ) ) )  -> 
( ( ( r  x.  z ) (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( 0 ( ball `  ( abs  o.  -  ) ) d ) )  =  (/) )
2142133exp2 1171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  ( r  x.  z
)  e.  CC  /\  0  e.  CC )  ->  ( r  e.  RR*  ->  ( d  e.  RR*  ->  ( ( r + e d )  <_ 
( ( r  x.  z ) ( abs 
o.  -  ) 0 )  ->  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  (
0 ( ball `  ( abs  o.  -  ) ) d ) )  =  (/) ) ) ) )
215214imp32 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  ( r  x.  z )  e.  CC  /\  0  e.  CC )  /\  ( r  e. 
RR*  /\  d  e.  RR* ) )  ->  (
( r + e
d )  <_  (
( r  x.  z
) ( abs  o.  -  ) 0 )  ->  ( ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r )  i^i  (
0 ( ball `  ( abs  o.  -  ) ) d ) )  =  (/) ) )
216208, 209, 210, 211, 212, 215syl32anc 1192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  ( (
r + e d )  <_  ( (
r  x.  z ) ( abs  o.  -  ) 0 )  -> 
( ( ( r  x.  z ) (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( 0 ( ball `  ( abs  o.  -  ) ) d ) )  =  (/) ) )
217 sseq0 3619 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( r  x.  z ) (
ball `  ( abs  o. 
-  ) ) r )  i^i  X ) 
C_  ( ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r )  i^i  (
0 ( ball `  ( abs  o.  -  ) ) d ) )  /\  ( ( ( r  x.  z ) (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( 0 ( ball `  ( abs  o.  -  ) ) d ) )  =  (/) )  ->  ( ( ( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =  (/) )
218207, 216, 217ee12an 1369 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  ( (
r + e d )  <_  ( (
r  x.  z ) ( abs  o.  -  ) 0 )  -> 
( ( ( r  x.  z ) (
ball `  ( abs  o. 
-  ) ) r )  i^i  X )  =  (/) ) )
219218necon3ad 2603 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  ( (
( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r )  i^i  X )  =/=  (/)  ->  -.  ( r + e d )  <_ 
( ( r  x.  z ) ( abs 
o.  -  ) 0 ) ) )
220219imp 419 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  ->  -.  ( r + e
d )  <_  (
( r  x.  z
) ( abs  o.  -  ) 0 ) )
221 rexadd 10774 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( r  e.  RR  /\  d  e.  RR )  ->  ( r + e
d )  =  ( r  +  d ) )
222189, 191, 221syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( r + e
d )  =  ( r  +  d ) )
223209adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( r  x.  z
)  e.  CC )
224125cnmetdval 18758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( r  x.  z
)  e.  CC  /\  0  e.  CC )  ->  ( ( r  x.  z ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( ( r  x.  z )  -  0 ) ) )
225223, 165, 224sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( r  x.  z ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( ( r  x.  z )  -  0 ) ) )
226223subid1d 9356 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( r  x.  z )  -  0 )  =  ( r  x.  z ) )
227226fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  (
( r  x.  z
)  -  0 ) )  =  ( abs `  ( r  x.  z
) ) )
228225, 227eqtrd 2436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( r  x.  z ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( r  x.  z
) ) )
229222, 228breq12d 4185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  /\  ( (
( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( r + e d )  <_ 
( ( r  x.  z ) ( abs 
o.  -  ) 0 )  <->  ( r  +  d )  <_  ( abs `  ( r  x.  z ) ) ) )
230220, 229mtbid 292 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( D  e.