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

Theorem cntotbnd 26507
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 26500 . 2  |-  ( D  e.  ( TotBnd `  X
)  ->  D  e.  ( Bnd `  X ) )
2 rpcn 10622 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  r  e.  CC )
32adantl 454 . . . . . . . . 9  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  r  e.  CC )
4 gzcn 13302 . . . . . . . . 9  |-  ( z  e.  ZZ [ _i ]  ->  z  e.  CC )
5 mulcl 9076 . . . . . . . . 9  |-  ( ( r  e.  CC  /\  z  e.  CC )  ->  ( r  x.  z
)  e.  CC )
63, 4, 5syl2an 465 . . . . . . . 8  |-  ( ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  /\  z  e.  ZZ [ _i ] )  -> 
( r  x.  z
)  e.  CC )
7 eqid 2438 . . . . . . . 8  |-  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  =  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )
86, 7fmptd 5895 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  (
z  e.  ZZ [
_i ]  |->  ( r  x.  z ) ) : ZZ [ _i ]
--> CC )
9 frn 5599 . . . . . . 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 9073 . . . . . . 7  |-  CC  e.  _V
1211elpw2 4366 . . . . . 6  |-  ( ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  e.  ~P CC  <->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  C_  CC )
1310, 12sylibr 205 . . . . 5  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  e.  ~P CC )
14 cnmet 18808 . . . . . . . . . . . . . . . . 17  |-  ( abs 
o.  -  )  e.  ( Met `  CC )
15 cntotbnd.d . . . . . . . . . . . . . . . . . 18  |-  D  =  ( ( abs  o.  -  )  |`  ( X  X.  X ) )
1615bnd2lem 26502 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs  o.  -  )  e.  ( Met `  CC )  /\  D  e.  ( Bnd `  X
) )  ->  X  C_  CC )
1714, 16mpan 653 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( Bnd `  X
)  ->  X  C_  CC )
1817sselda 3350 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  y  e.  X )  ->  y  e.  CC )
1918adantrl 698 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
y  e.  CC )
2019recld 12001 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Re `  y
)  e.  RR )
21 simprl 734 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR+ )
2220, 21rerpdivcld 10677 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  y )  /  r
)  e.  RR )
23 1re 9092 . . . . . . . . . . . . 13  |-  1  e.  RR
2423rehalfcli 10218 . . . . . . . . . . . 12  |-  ( 1  /  2 )  e.  RR
25 readdcl 9075 . . . . . . . . . . . 12  |-  ( ( ( ( Re `  y )  /  r
)  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) )  e.  RR )
2622, 24, 25sylancl 645 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) )  e.  RR )
2726flcld 11209 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ )
2819imcld 12002 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Im `  y
)  e.  RR )
2928, 21rerpdivcld 10677 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Im `  y )  /  r
)  e.  RR )
30 readdcl 9075 . . . . . . . . . . . 12  |-  ( ( ( ( Im `  y )  /  r
)  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) )  e.  RR )
3129, 24, 30sylancl 645 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) )  e.  RR )
3231flcld 11209 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ )
33 gzreim 13309 . . . . . . . . . 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 644 . . . . . . . . 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 13302 . . . . . . . . . . . . . . 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 10652 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  CC )
3821rpne0d 10655 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  =/=  0 )
3919, 37, 38divcld 9792 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  e.  CC )
4036, 39subcld 9413 . . . . . . . . . . . . 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 12240 . . . . . . . . . . . 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 10378 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  CC )
44 ax-icn 9051 . . . . . . . . . . . . . . . . . . . . 21  |-  _i  e.  CC
4532zcnd 10378 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  CC )
46 mulcl 9076 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( _i  e.  CC  /\  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  e.  CC )  -> 
( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  e.  CC )
4744, 45, 46sylancr 646 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  e.  CC )
4822recnd 9116 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  y )  /  r
)  e.  CC )
4929recnd 9116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Im `  y )  /  r
)  e.  CC )
50 mulcl 9076 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( _i  e.  CC  /\  ( ( Im `  y )  /  r
)  e.  CC )  ->  ( _i  x.  ( ( Im `  y )  /  r
) )  e.  CC )
5144, 49, 50sylancr 646 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
( Im `  y
)  /  r ) )  e.  CC )
5243, 47, 48, 51addsub4d 9460 . . . . . . . . . . . . . . . . . . 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 12004 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  =  ( ( Re `  ( y  /  r ) )  +  ( _i  x.  ( Im `  ( y  /  r ) ) ) ) )
5421rpred 10650 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR )
5554, 19, 38redivd 12036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Re `  (
y  /  r ) )  =  ( ( Re `  y )  /  r ) )
5654, 19, 38imdivd 12037 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Im `  (
y  /  r ) )  =  ( ( Im `  y )  /  r ) )
5756oveq2d 6099 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
Im `  ( y  /  r ) ) )  =  ( _i  x.  ( ( Im
`  y )  / 
r ) ) )
5855, 57oveq12d 6101 . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  =  ( ( ( Re `  y
)  /  r )  +  ( _i  x.  ( ( Im `  y )  /  r
) ) ) )
6059oveq2d 6099 . . . . . . . . . . . . . . . . . . 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 9491 . . . . . . . . . . . . . . . . . . . 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 6099 . . . . . . . . . . . . . . . . . . 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 2480 . . . . . . . . . . . . . . . . . 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 5734 . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . 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 10377 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  RR )
6867, 22resubcld 9467 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  RR )
6932zred 10377 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  RR )
7069, 29resubcld 9467 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  RR )
71 absreimsq 12099 . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . 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 11551 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  e.  RR )
7570resqcld 11551 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  e.  RR )
7624resqcli 11469 . . . . . . . . . . . . . . . . . 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 12109 . . . . . . . . . . . . . . . . . . 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 12146 . . . . . . . . . . . . . . . . . . . 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 9116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  CC )
8483abscld 12240 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) )  e.  RR )
8583absge0d 12248 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( abs `  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) ) ) )
86 halfgt0 10190 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  ( 1  /  2
)
8724, 86elrpii 10617 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  e.  RR+
88 rpge0 10626 . . . . . . . . . . . . . . . . . . . . 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 11560 . . . . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . . . . 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 4236 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  <_  ( (
1  /  2 ) ^ 2 ) )
9324recni 9104 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  2 )  e.  CC
9493sqvali 11463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 ) ^ 2 )  =  ( ( 1  / 
2 )  x.  (
1  /  2 ) )
95 halflt1 10191 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  <  1
9624, 23, 24, 86ltmul1ii 9941 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  /  2 )  <  1  <->  ( (
1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  x.  (
1  /  2 ) ) )
9795, 96mpbi 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  x.  (
1  /  2 ) )
9893mulid2i 9095 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  x.  ( 1  / 
2 ) )  =  ( 1  /  2
)
9997, 98breqtri 4237 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  /  2
)
10094, 99eqbrtri 4233 . . . . . . . . . . . . . . . . . 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 9230 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  <  ( 1  /  2 ) )
103 absresq 12109 . . . . . . . . . . . . . . . . . . 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 12146 . . . . . . . . . . . . . . . . . . . 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 9116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  CC )
108107abscld 12240 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  e.  RR )
109107absge0d 12248 . . . . . . . . . . . . . . . . . . . 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 11560 . . . . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . . . . 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 4236 . . . . . . . . . . . . . . . . 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 9230 . . . . . . . . . . . . . . . 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 10217 . . . . . . . . . . . . . . 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 4234 . . . . . . . . . . . . . 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 11478 . . . . . . . . . . . . . 14  |-  ( 1 ^ 2 )  =  1
117115, 116syl6breqr 4254 . . . . . . . . . . . . 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 12248 . . . . . . . . . . . . . 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 9553 . . . . . . . . . . . . . . 15  |-  0  <_  1
120119a1i 11 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  1 )
12141, 42, 118, 120lt2sqd 11559 . . . . . . . . . . . . 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 225 . . . . . . . . . . . 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 10702 . . . . . . . . . . 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 9110 . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . 14  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
126125cnmetdval 18807 . . . . . . . . . . . . 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 644 . . . . . . . . . . . 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 9491 . . . . . . . . . . . . . . 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 9794 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  (
y  /  r ) )  =  y )
130129oveq2d 6099 . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . 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 5734 . . . . . . . . . . . . 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 12258 . . . . . . . . . . . . 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 2472 . . . . . . . . . . . 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 10654 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  r )
13654, 135absidd 12227 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  r
)  =  r )
137136oveq1d 6098 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 9107 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  1 )  =  r )
140123, 138, 1393brtr3d 4243 . . . . . . . . . 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 18809 . . . . . . . . . . . 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 10621 . . . . . . . . . . . 12  |-  ( r  e.  RR+  ->  r  e. 
RR* )
144143ad2antrl 710 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR* )
145 elbl2 18422 . . . . . . . . . . 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 1186 . . . . . . . . . 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 225 . . . . . . . . 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 6091 . . . . . . . . . . . 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 6098 . . . . . . . . . . 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 2505 . . . . . . . . . 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 3054 . . . . . . . . 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 644 . . . . . . . 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 600 . . . . . . 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 4099 . . . . . . . 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 6108 . . . . . . . . . 10  |-  ( r  x.  z )  e. 
_V
156155rgenw 2775 . . . . . . . . 9  |-  A. z  e.  ZZ [ _i ] 
( r  x.  z
)  e.  _V
157 oveq1 6090 . . . . . . . . . . 11  |-  ( x  =  ( r  x.  z )  ->  (
x ( ball `  ( abs  o.  -  ) ) r )  =  ( ( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r ) )
158157eleq2d 2505 . . . . . . . . . 10  |-  ( x  =  ( r  x.  z )  ->  (
y  e.  ( x ( ball `  ( abs  o.  -  ) ) r )  <->  y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) ) )
1597, 158rexrnmpt 5881 . . . . . . . . 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 242 . . . . . . 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 220 . . . . . 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 3356 . . . . 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 445 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  D  e.  ( Bnd `  X
) )
165 0cn 9086 . . . . . . . 8  |-  0  e.  CC
16615ssbnd 26499 . . . . . . . 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 655 . . . . . . 7  |-  ( D  e.  ( Bnd `  X
)  <->  E. d  e.  RR  X  C_  ( 0 (
ball `  ( abs  o. 
-  ) ) d ) )
168164, 167sylib 190 . . . . . 6  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  E. d  e.  RR  X  C_  (
0 ( ball `  ( abs  o.  -  ) ) d ) )
169 fzfi 11313 . . . . . . . . 9  |-  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) )  e.  Fin
170 xpfi 7380 . . . . . . . . 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 655 . . . . . . . 8  |-  ( (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) )  e.  Fin
172 eqid 2438 . . . . . . . . . 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 6108 . . . . . . . . . 10  |-  ( r  x.  ( a  +  ( _i  x.  b
) ) )  e. 
_V
174172, 173fnmpt2i 6422 . . . . . . . . 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 5661 . . . . . . . . 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 201 . . . . . . . 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 7394 . . . . . . . 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 655 . . . . . . 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 5123 . . . . . . . . . 10  |-  ( x  e.  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  <->  E. z  e.  ZZ [ _i ]  x  =  ( r  x.  z ) )
180 elgz 13301 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  ZZ [ _i ] 
<->  ( z  e.  CC  /\  ( Re `  z
)  e.  ZZ  /\  ( Im `  z )  e.  ZZ ) )
181180simp2bi 974 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ZZ [ _i ]  ->  ( Re `  z )  e.  ZZ )
182181ad2antlr 709 . . . . . . . . . . . . . . . . . . . 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 10378 . . . . . . . . . . . . . . . . . . 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 12240 . . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . . . 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 12240 . . . . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . 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 10650 . . . . . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . 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 9117 . . . . . . . . . . . . . . . . . . . . . 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 10677 . . . . . . . . . . . . . . . . . . . . 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 11209 . . . . . . . . . . . . . . . . . . . 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 10380 . . . . . . . . . . . . . . . . . . 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 10377 . . . . . . . . . . . . . . . . . 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 12115 . . . . . . . . . . . . . . . . . . 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 10652 . . . . . . . . . . . . . . . . . . . . . . . 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 12258 . . . . . . . . . . . . . . . . . . . . . . 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 10654 . . . . . . . . . . . . . . . . . . . . . . . . 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 12227 . . . . . . . . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3569 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 18430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1193 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3661 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . . . . . . . . . . . . . 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 420 . . . . . . . . . . . . . . . . . . . . . . . 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 10820 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( r  e.  RR  /\  d  e.  RR )  ->  ( r + e
d )  =  ( r  +  d ) )
222189, 191, 221syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 18807 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( r  x.  z
)  e.  CC  /\  0  e.  CC )  ->  ( ( r  x.  z ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( ( r  x.  z )  -  0 ) ) )
225223, 165, 224sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . 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 9402 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5734 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . . . . . . 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 4227 . . . . . . . . . . . . . . . . . . . . . . . 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 293 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( D