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

Theorem cntotbnd 26520
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 26513 . 2  |-  ( D  e.  ( TotBnd `  X
)  ->  D  e.  ( Bnd `  X ) )
2 rpcn 10362 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  r  e.  CC )
32adantl 452 . . . . . . . . 9  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  r  e.  CC )
4 gzcn 12979 . . . . . . . . 9  |-  ( z  e.  ZZ [ _i ]  ->  z  e.  CC )
5 mulcl 8821 . . . . . . . . 9  |-  ( ( r  e.  CC  /\  z  e.  CC )  ->  ( r  x.  z
)  e.  CC )
63, 4, 5syl2an 463 . . . . . . . 8  |-  ( ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  /\  z  e.  ZZ [ _i ] )  -> 
( r  x.  z
)  e.  CC )
7 eqid 2283 . . . . . . . 8  |-  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  =  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )
86, 7fmptd 5684 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  (
z  e.  ZZ [
_i ]  |->  ( r  x.  z ) ) : ZZ [ _i ]
--> CC )
9 frn 5395 . . . . . . 7  |-  ( ( z  e.  ZZ [
_i ]  |->  ( r  x.  z ) ) : ZZ [ _i ]
--> CC  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  C_  CC )
108, 9syl 15 . . . . . 6  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) ) 
C_  CC )
11 cnex 8818 . . . . . . 7  |-  CC  e.  _V
1211elpw2 4175 . . . . . 6  |-  ( ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  e.  ~P CC  <->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  C_  CC )
1310, 12sylibr 203 . . . . 5  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  e.  ~P CC )
14 cnmet 18281 . . . . . . . . . . . . . . . . 17  |-  ( abs 
o.  -  )  e.  ( Met `  CC )
15 cntotbnd.d . . . . . . . . . . . . . . . . . 18  |-  D  =  ( ( abs  o.  -  )  |`  ( X  X.  X ) )
1615bnd2lem 26515 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs  o.  -  )  e.  ( Met `  CC )  /\  D  e.  ( Bnd `  X
) )  ->  X  C_  CC )
1714, 16mpan 651 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( Bnd `  X
)  ->  X  C_  CC )
1817sselda 3180 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  y  e.  X )  ->  y  e.  CC )
1918adantrl 696 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
y  e.  CC )
2019recld 11679 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Re `  y
)  e.  RR )
21 simprl 732 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR+ )
2220, 21rerpdivcld 10417 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  y )  /  r
)  e.  RR )
23 1re 8837 . . . . . . . . . . . . 13  |-  1  e.  RR
24 rehalfcl 9938 . . . . . . . . . . . . 13  |-  ( 1  e.  RR  ->  (
1  /  2 )  e.  RR )
2523, 24ax-mp 8 . . . . . . . . . . . 12  |-  ( 1  /  2 )  e.  RR
26 readdcl 8820 . . . . . . . . . . . 12  |-  ( ( ( ( Re `  y )  /  r
)  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) )  e.  RR )
2722, 25, 26sylancl 643 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) )  e.  RR )
2827flcld 10930 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ )
2919imcld 11680 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Im `  y
)  e.  RR )
3029, 21rerpdivcld 10417 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Im `  y )  /  r
)  e.  RR )
31 readdcl 8820 . . . . . . . . . . . 12  |-  ( ( ( ( Im `  y )  /  r
)  e.  RR  /\  ( 1  /  2
)  e.  RR )  ->  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) )  e.  RR )
3230, 25, 31sylancl 643 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) )  e.  RR )
3332flcld 10930 . . . . . . . . . 10  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  ZZ )
34 gzreim 12986 . . . . . . . . . 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 ] )
3528, 33, 34syl2anc 642 . . . . . . . . 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 ] )
36 gzcn 12979 . . . . . . . . . . . . . . 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 )
3735, 36syl 15 . . . . . . . . . . . . . 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 )
3821rpcnd 10392 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  CC )
3921rpne0d 10395 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  =/=  0 )
4019, 38, 39divcld 9536 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  e.  CC )
4137, 40subcld 9157 . . . . . . . . . . . . 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 )
4241abscld 11918 . . . . . . . . . . . 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 )
4323a1i 10 . . . . . . . . . . . 12  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
1  e.  RR )
4428zcnd 10118 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  CC )
45 ax-icn 8796 . . . . . . . . . . . . . . . . . . . . 21  |-  _i  e.  CC
4633zcnd 10118 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  CC )
47 mulcl 8821 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( _i  e.  CC  /\  ( |_ `  ( ( ( Im `  y
)  /  r )  +  ( 1  / 
2 ) ) )  e.  CC )  -> 
( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  e.  CC )
4845, 46, 47sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  ( |_ `  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) ) )  e.  CC )
4922recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Re `  y )  /  r
)  e.  CC )
5030recnd 8861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( Im `  y )  /  r
)  e.  CC )
51 mulcl 8821 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( _i  e.  CC  /\  ( ( Im `  y )  /  r
)  e.  CC )  ->  ( _i  x.  ( ( Im `  y )  /  r
) )  e.  CC )
5245, 50, 51sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
( Im `  y
)  /  r ) )  e.  CC )
5344, 48, 49, 52addsub4d 9204 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
5440replimd 11682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  =  ( ( Re `  ( y  /  r ) )  +  ( _i  x.  ( Im `  ( y  /  r ) ) ) ) )
5521rpred 10390 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR )
5655, 19, 39redivd 11714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Re `  (
y  /  r ) )  =  ( ( Re `  y )  /  r ) )
5755, 19, 39imdivd 11715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( Im `  (
y  /  r ) )  =  ( ( Im `  y )  /  r ) )
5857oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( _i  x.  (
Im `  ( y  /  r ) ) )  =  ( _i  x.  ( ( Im
`  y )  / 
r ) ) )
5956, 58oveq12d 5876 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
6054, 59eqtrd 2315 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( y  /  r
)  =  ( ( ( Re `  y
)  /  r )  +  ( _i  x.  ( ( Im `  y )  /  r
) ) ) )
6160oveq2d 5874 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
6245a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  ->  _i  e.  CC )
6362, 46, 50subdid 9235 . . . . . . . . . . . . . . . . . . . 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
) ) ) )
6463oveq2d 5874 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
6553, 61, 643eqtr4d 2325 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
6665fveq2d 5529 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
6766oveq1d 5873 . . . . . . . . . . . . . . . 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 ) )
6828zred 10117 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  RR )
6968, 22resubcld 9211 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  RR )
7033zred 10117 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  e.  RR )
7170, 30resubcld 9211 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  RR )
72 absreimsq 11777 . . . . . . . . . . . . . . . . 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 ) ) )
7369, 71, 72syl2anc 642 . . . . . . . . . . . . . . . 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 ) ) )
7467, 73eqtrd 2315 . . . . . . . . . . . . . . 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 ) ) )
7569resqcld 11271 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  e.  RR )
7671resqcld 11271 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  e.  RR )
7725resqcli 11189 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  /  2 ) ^ 2 )  e.  RR
7877a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( 1  / 
2 ) ^ 2 )  e.  RR )
7925a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( 1  /  2
)  e.  RR )
80 absresq 11787 . . . . . . . . . . . . . . . . . . 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 ) )
8169, 80syl 15 . . . . . . . . . . . . . . . . . 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 ) )
82 rddif 11824 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Re `  y
)  /  r )  e.  RR  ->  ( abs `  ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) )  <_ 
( 1  /  2
) )
8322, 82syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) )  <_  ( 1  /  2 ) )
8469recnd 8861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) )  e.  CC )
8584abscld 11918 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) )  e.  RR )
8684absge0d 11926 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( abs `  ( ( |_ `  ( ( ( Re
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Re `  y
)  /  r ) ) ) )
87 halfgt0 9932 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  ( 1  /  2
)
8825, 87elrpii 10357 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  e.  RR+
89 rpge0 10366 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  /  2 )  e.  RR+  ->  0  <_ 
( 1  /  2
) )
9088, 89mp1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( 1  /  2 ) )
9185, 79, 86, 90le2sqd 11280 . . . . . . . . . . . . . . . . . . 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 ) ) )
9283, 91mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Re `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Re `  y )  /  r ) ) ) ^ 2 )  <_  ( ( 1  /  2 ) ^
2 ) )
9381, 92eqbrtrrd 4045 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  <_  ( (
1  /  2 ) ^ 2 ) )
9425recni 8849 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  2 )  e.  CC
9594sqvali 11183 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 ) ^ 2 )  =  ( ( 1  / 
2 )  x.  (
1  /  2 ) )
96 halflt1 9933 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  <  1
9725, 23, 25, 87ltmul1ii 9685 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  /  2 )  <  1  <->  ( (
1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  x.  (
1  /  2 ) ) )
9896, 97mpbi 199 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  x.  (
1  /  2 ) )
9994mulid2i 8840 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  x.  ( 1  / 
2 ) )  =  ( 1  /  2
)
10098, 99breqtri 4046 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 )  x.  ( 1  / 
2 ) )  < 
( 1  /  2
)
10195, 100eqbrtri 4042 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  /  2 ) ^ 2 )  < 
( 1  /  2
)
102101a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( 1  / 
2 ) ^ 2 )  <  ( 1  /  2 ) )
10375, 78, 79, 93, 102lelttrd 8974 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Re `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Re `  y )  /  r
) ) ^ 2 )  <  ( 1  /  2 ) )
104 absresq 11787 . . . . . . . . . . . . . . . . . . 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 ) )
10571, 104syl 15 . . . . . . . . . . . . . . . . . 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 ) )
106 rddif 11824 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Im `  y
)  /  r )  e.  RR  ->  ( abs `  ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) )  <_ 
( 1  /  2
) )
10730, 106syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  <_  ( 1  /  2 ) )
10871recnd 8861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) )  e.  CC )
109108abscld 11918 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) )  e.  RR )
110108absge0d 11926 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  ( abs `  ( ( |_ `  ( ( ( Im
`  y )  / 
r )  +  ( 1  /  2 ) ) )  -  (
( Im `  y
)  /  r ) ) ) )
111109, 79, 110, 90le2sqd 11280 . . . . . . . . . . . . . . . . . . 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 ) ) )
112107, 111mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( abs `  (
( |_ `  (
( ( Im `  y )  /  r
)  +  ( 1  /  2 ) ) )  -  ( ( Im `  y )  /  r ) ) ) ^ 2 )  <_  ( ( 1  /  2 ) ^
2 ) )
113105, 112eqbrtrrd 4045 . . . . . . . . . . . . . . . . 17  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  <_  ( (
1  /  2 ) ^ 2 ) )
11476, 78, 79, 113, 102lelttrd 8974 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( ( ( |_
`  ( ( ( Im `  y )  /  r )  +  ( 1  /  2
) ) )  -  ( ( Im `  y )  /  r
) ) ^ 2 )  <  ( 1  /  2 ) )
11575, 76, 43, 103, 114lt2halvesd 9959 . . . . . . . . . . . . . . 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 )
11674, 115eqbrtrd 4043 . . . . . . . . . . . . . 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 )
117 sq1 11198 . . . . . . . . . . . . . 14  |-  ( 1 ^ 2 )  =  1
118116, 117syl6breqr 4063 . . . . . . . . . . . . 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 ) )
11941absge0d 11926 . . . . . . . . . . . . . 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 ) ) ) )
120 0le1 9297 . . . . . . . . . . . . . . 15  |-  0  <_  1
121120a1i 10 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  1 )
12242, 43, 119, 121lt2sqd 11279 . . . . . . . . . . . . 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 ) ) )
123118, 122mpbird 223 . . . . . . . . . . . 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 )
12442, 43, 21, 123ltmul2dd 10442 . . . . . . . . . . 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 ) )
12538, 37mulcld 8855 . . . . . . . . . . . . 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 )
126 eqid 2283 . . . . . . . . . . . . . 14  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
127126cnmetdval 18280 . . . . . . . . . . . . 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
) ) )
128125, 19, 127syl2anc 642 . . . . . . . . . . . 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
) ) )
12938, 37, 40subdid 9235 . . . . . . . . . . . . . . 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 ) ) ) )
13019, 38, 39divcan2d 9538 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  (
y  /  r ) )  =  y )
131130oveq2d 5874 . . . . . . . . . . . . . . 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 ) )
132129, 131eqtrd 2315 . . . . . . . . . . . . . 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 ) )
133132fveq2d 5529 . . . . . . . . . . . . 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
) ) )
13438, 41absmuld 11936 . . . . . . . . . . . . 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 ) ) ) ) )
135133, 134eqtr3d 2317 . . . . . . . . . . . 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 ) ) ) ) )
13621rpge0d 10394 . . . . . . . . . . . . . 14  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
0  <_  r )
13755, 136absidd 11905 . . . . . . . . . . . . 13  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs `  r
)  =  r )
138137oveq1d 5873 . . . . . . . . . . . 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 ) ) ) ) )
139128, 135, 1383eqtrrd 2320 . . . . . . . . . . 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
) )
14038mulid1d 8852 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( r  x.  1 )  =  r )
141124, 139, 1403brtr3d 4052 . . . . . . . . . 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 )
142 cnxmet 18282 . . . . . . . . . . . 12  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
143142a1i 10 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
( abs  o.  -  )  e.  ( * Met `  CC ) )
144 rpxr 10361 . . . . . . . . . . . 12  |-  ( r  e.  RR+  ->  r  e. 
RR* )
145144ad2antrl 708 . . . . . . . . . . 11  |-  ( ( D  e.  ( Bnd `  X )  /\  (
r  e.  RR+  /\  y  e.  X ) )  -> 
r  e.  RR* )
146 elbl2 17950 . . . . . . . . . . 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 )
)
147143, 145, 125, 19, 146syl22anc 1183 . . . . . . . . . 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
) )
148141, 147mpbird 223 . . . . . . . . 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 ) )
149 oveq2 5866 . . . . . . . . . . . 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 ) ) ) ) ) ) )
150149oveq1d 5873 . . . . . . . . . . 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 ) )
151150eleq2d 2350 . . . . . . . . . 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 ) ) )
152151rspcev 2884 . . . . . . . . 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 ) )
15335, 148, 152syl2anc 642 . . . . . . . 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 ) )
154153expr 598 . . . . . . 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 ) ) )
155 eliun 3909 . . . . . . . 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 ) )
156 ovex 5883 . . . . . . . . . 10  |-  ( r  x.  z )  e. 
_V
157156rgenw 2610 . . . . . . . . 9  |-  A. z  e.  ZZ [ _i ] 
( r  x.  z
)  e.  _V
158 oveq1 5865 . . . . . . . . . . 11  |-  ( x  =  ( r  x.  z )  ->  (
x ( ball `  ( abs  o.  -  ) ) r )  =  ( ( r  x.  z
) ( ball `  ( abs  o.  -  ) ) r ) )
159158eleq2d 2350 . . . . . . . . . 10  |-  ( x  =  ( r  x.  z )  ->  (
y  e.  ( x ( ball `  ( abs  o.  -  ) ) r )  <->  y  e.  ( ( r  x.  z ) ( ball `  ( abs  o.  -  ) ) r ) ) )
1607, 159rexrnmpt 5670 . . . . . . . . 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 ) ) )
161157, 160ax-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 ) )
162155, 161bitri 240 . . . . . . 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 ) )
163154, 162syl6ibr 218 . . . . . 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 ) ) )
164163ssrdv 3185 . . . . 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 ) )
165 simpl 443 . . . . . . 7  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  D  e.  ( Bnd `  X
) )
166 0cn 8831 . . . . . . . 8  |-  0  e.  CC
16715ssbnd 26512 . . . . . . . 8  |-  ( ( ( abs  o.  -  )  e.  ( Met `  CC )  /\  0  e.  CC )  ->  ( D  e.  ( Bnd `  X )  <->  E. d  e.  RR  X  C_  (
0 ( ball `  ( abs  o.  -  ) ) d ) ) )
16814, 166, 167mp2an 653 . . . . . . 7  |-  ( D  e.  ( Bnd `  X
)  <->  E. d  e.  RR  X  C_  ( 0 (
ball `  ( abs  o. 
-  ) ) d ) )
169165, 168sylib 188 . . . . . 6  |-  ( ( D  e.  ( Bnd `  X )  /\  r  e.  RR+ )  ->  E. d  e.  RR  X  C_  (
0 ( ball `  ( abs  o.  -  ) ) d ) )
170 fzfi 11034 . . . . . . . . . . 11  |-  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) )  e.  Fin
171 xpfi 7128 . . . . . . . . . . 11  |-  ( ( ( -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 )
172170, 170, 171mp2an 653 . . . . . . . . . 10  |-  ( (
-u ( ( |_
`  ( ( r  +  d )  / 
r ) )  +  1 ) ... (
( |_ `  (
( r  +  d )  /  r ) )  +  1 ) )  X.  ( -u ( ( |_ `  ( ( r  +  d )  /  r
) )  +  1 ) ... ( ( |_ `  ( ( r  +  d )  /  r ) )  +  1 ) ) )  e.  Fin
173 eqid 2283 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
174 ovex 5883 . . . . . . . . . . . 12  |-  ( r  x.  ( a  +  ( _i  x.  b
) ) )  e. 
_V
175173, 174fnmpt2i 6193 . . . . . . . . . . 11  |-  ( 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 ) ) )
176 dffn4 5457 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) )
177175, 176mpbi 199 . . . . . . . . . 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 ) ) ) ) : ( ( -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 ) ) ) )
178 fofi 7142 . . . . . . . . . 10  |-  ( ( ( ( -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 )
179172, 177, 178mp2an 653 . . . . . . . . 9  |-  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
1807, 156elrnmpti 4930 . . . . . . . . . . . 12  |-  ( x  e.  ran  ( z  e.  ZZ [ _i ]  |->  ( r  x.  z ) )  <->  E. z  e.  ZZ [ _i ]  x  =  ( r  x.  z ) )
181 elgz 12978 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  ZZ [ _i ] 
<->  ( z  e.  CC  /\  ( Re `  z
)  e.  ZZ  /\  ( Im `  z )  e.  ZZ ) )
182181simp2bi 971 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ZZ [ _i ]  ->  ( Re `  z )  e.  ZZ )
183182ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( Re `  z
)  e.  ZZ )
184183zcnd 10118 . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( Re `  z
)  e.  CC )
185184abscld 11918 . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( abs `  (
Re `  z )
)  e.  RR )
1864ad2antlr 707 . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
z  e.  CC )
187186abscld 11918 . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( abs `  z
)  e.  RR )
188 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  r  e.  RR+ )
189188adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 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  e.  RR+ )
190189rpred 10390 . . . . . . . . . . . . . . . . . . . . . . . . 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.  RR )
191 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  d  e.  RR )
192191adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
d  e.  RR )
193190, 192readdcld 8862 . . . . . . . . . . . . . . . . . . . . . . . 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  +  d )  e.  RR )
194193, 189rerpdivcld 10417 . . . . . . . . . . . . . . . . . . . . . . 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  +  d )  /  r
)  e.  RR )
195194flcld 10930 . . . . . . . . . . . . . . . . . . . . . 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 )  /  r ) )  e.  ZZ )
196195peano2zd 10120 . . . . . . . . . . . . . . . . . . . . 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
) )  +  1 )  e.  ZZ )
197196zred 10117 . . . . . . . . . . . . . . . . . . . 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
) )  +  1 )  e.  RR )
198 absrele 11793 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  CC  ->  ( abs `  ( Re `  z ) )  <_ 
( abs `  z
) )
199186, 198syl 15 . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( abs `  (
Re `  z )
)  <_  ( abs `  z ) )
200189rpcnd 10392 . . . . . . . . . . . . . . . . . . . . . . . . . 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  e.  CC )
201200, 186absmuld 11936 . . . . . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( abs `  (
r  x.  z ) )  =  ( ( abs `  r )  x.  ( abs `  z
) ) )
202189rpge0d 10394 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
0  <_  r )
203190, 202absidd 11905 . . . . . . . . . . . . . . . . . . . . . . . . . 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
)  =  r )
204203oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . 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
)  =/=  (/) )  -> 
( ( abs `  r
)  x.  ( abs `  z ) )  =  ( r  x.  ( abs `  z ) ) )
205201, 204eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . 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  x.  z ) )  =  ( r  x.  ( abs `  z
) ) )
206 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 ) )
207 sslin 3395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) )
208206, 207syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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 ) ) )
209142a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 ) )
2106adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 )
211166a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  0  e.  CC )
212188, 144syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  r  e.  RR* )
213191rexrd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  ) ) d ) ) )  /\  z  e.  ZZ [ _i ]
)  ->  d  e.  RR* )
214 bldisj 17955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 ) )  =  (/) )
2152143exp2 1169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 ) )  =  (/) ) ) ) )
216215imp32 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  =  (/) ) )
217209, 210, 211, 212, 213, 216syl32anc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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 ) )  =  (/) ) )
218 sseq0 3486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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
)  =  (/) )
219208, 217, 218ee12an 1353 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )  =  (/) ) )
220219necon3ad 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 + e d )  <_ 
( ( r  x.  z ) ( abs 
o.  -  ) 0 ) ) )
221220imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . 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 + e
d )  <_  (
( r  x.  z
) ( abs  o.  -  ) 0 ) )
222 rexadd 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( r  e.  RR  /\  d  e.  RR )  ->  ( r + e
d )  =  ( r  +  d ) )
223190, 192, 222syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 + e
d )  =  ( r  +  d ) )
224210adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 )
225126cnmetdval 18280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( r  x.  z
)  e.  CC  /\  0  e.  CC )  ->  ( ( r  x.  z ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( ( r  x.  z )  -  0 ) ) )
226224, 166, 225sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( ( r  x.  z ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( ( r  x.  z )  -  0 ) ) )
227224subid1d 9146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 ) )
228227fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ( ball `  ( abs  o.  -  ) ) r )  i^i  X
)  =/=  (/) )  -> 
( abs `  (
( r  x.  z
)  -  0 ) )  =  ( abs `  ( r  x.  z
) ) )
229226, 228eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ( abs 
o.  -  ) 0 )  =  ( abs `  ( r  x.  z
) ) )
230223, 229breq12d 4036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( D  e.  ( Bnd `  X
)  /\  r  e.  RR+ )  /\  ( d  e.  RR  /\  X  C_  ( 0 ( ball `  ( abs  o.  -  )