This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cntotbnd

Description: A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis cntotbnd.d 
|- D = ( ( abs o. - ) |` ( X X. X ) )
Assertion cntotbnd 
|- ( D e. ( TotBnd ` X ) <-> D e. ( Bnd ` X ) )

Proof

Step Hyp Ref Expression
1 cntotbnd.d 
 |-  D = ( ( abs o. - ) |` ( X X. X ) )
2 totbndbnd 
 |-  ( D e. ( TotBnd ` X ) -> D e. ( Bnd ` X ) )
3 rpcn 
 |-  ( r e. RR+ -> r e. CC )
4 3 adantl 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> r e. CC )
5 gzcn 
 |-  ( z e. Z[i] -> z e. CC )
6 mulcl 
 |-  ( ( r e. CC /\ z e. CC ) -> ( r x. z ) e. CC )
7 4 5 6 syl2an 
 |-  ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ z e. Z[i] ) -> ( r x. z ) e. CC )
8 7 fmpttd 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> ( z e. Z[i] |-> ( r x. z ) ) : Z[i] --> CC )
9 8 frnd 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> ran ( z e. Z[i] |-> ( r x. z ) ) C_ CC )
10 cnex 
 |-  CC e. _V
11 10 elpw2 
 |-  ( ran ( z e. Z[i] |-> ( r x. z ) ) e. ~P CC <-> ran ( z e. Z[i] |-> ( r x. z ) ) C_ CC )
12 9 11 sylibr 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> ran ( z e. Z[i] |-> ( r x. z ) ) e. ~P CC )
13 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
14 1 bnd2lem 
 |-  ( ( ( abs o. - ) e. ( Met ` CC ) /\ D e. ( Bnd ` X ) ) -> X C_ CC )
15 13 14 mpan 
 |-  ( D e. ( Bnd ` X ) -> X C_ CC )
16 15 sselda 
 |-  ( ( D e. ( Bnd ` X ) /\ y e. X ) -> y e. CC )
17 16 adantrl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> y e. CC )
18 17 recld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( Re ` y ) e. RR )
19 simprl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> r e. RR+ )
20 18 19 rerpdivcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( Re ` y ) / r ) e. RR )
21 halfre 
 |-  ( 1 / 2 ) e. RR
22 readdcl 
 |-  ( ( ( ( Re ` y ) / r ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) e. RR )
23 20 21 22 sylancl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) e. RR )
24 23 flcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) e. ZZ )
25 17 imcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( Im ` y ) e. RR )
26 25 19 rerpdivcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( Im ` y ) / r ) e. RR )
27 readdcl 
 |-  ( ( ( ( Im ` y ) / r ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) e. RR )
28 26 21 27 sylancl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) e. RR )
29 28 flcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) e. ZZ )
30 gzreim 
 |-  ( ( ( |_ ` ( ( ( 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. Z[i] )
31 24 29 30 syl2anc 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) + ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) ) e. Z[i] )
32 gzcn 
 |-  ( ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) + ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) ) e. Z[i] -> ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) + ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) ) e. CC )
33 31 32 syl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) + ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) ) e. CC )
34 19 rpcnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> r e. CC )
35 19 rpne0d 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> r =/= 0 )
36 17 34 35 divcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( y / r ) e. CC )
37 33 36 subcld 
 |-  ( ( 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 )
38 37 abscld 
 |-  ( ( 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 )
39 1re 
 |-  1 e. RR
40 39 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> 1 e. RR )
41 24 zcnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) e. CC )
42 ax-icn 
 |-  _i e. CC
43 29 zcnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) e. CC )
44 mulcl 
 |-  ( ( _i e. CC /\ ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) e. CC ) -> ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) e. CC )
45 42 43 44 sylancr 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) e. CC )
46 20 recnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( Re ` y ) / r ) e. CC )
47 26 recnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( Im ` y ) / r ) e. CC )
48 mulcl 
 |-  ( ( _i e. CC /\ ( ( Im ` y ) / r ) e. CC ) -> ( _i x. ( ( Im ` y ) / r ) ) e. CC )
49 42 47 48 sylancr 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( _i x. ( ( Im ` y ) / r ) ) e. CC )
50 41 45 46 49 addsub4d 
 |-  ( ( 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 ) ) ) ) )
51 36 replimd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( y / r ) = ( ( Re ` ( y / r ) ) + ( _i x. ( Im ` ( y / r ) ) ) ) )
52 19 rpred 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> r e. RR )
53 52 17 35 redivd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( Re ` ( y / r ) ) = ( ( Re ` y ) / r ) )
54 52 17 35 imdivd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( Im ` ( y / r ) ) = ( ( Im ` y ) / r ) )
55 54 oveq2d 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( _i x. ( Im ` ( y / r ) ) ) = ( _i x. ( ( Im ` y ) / r ) ) )
56 53 55 oveq12d 
 |-  ( ( 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 ) ) ) )
57 51 56 eqtrd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( y / r ) = ( ( ( Re ` y ) / r ) + ( _i x. ( ( Im ` y ) / r ) ) ) )
58 57 oveq2d 
 |-  ( ( 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 ) ) ) ) )
59 42 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> _i e. CC )
60 59 43 47 subdid 
 |-  ( ( 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 ) ) ) )
61 60 oveq2d 
 |-  ( ( 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 ) ) ) ) )
62 50 58 61 3eqtr4d 
 |-  ( ( 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 ) ) ) ) )
63 62 fveq2d 
 |-  ( ( 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 ) ) ) ) ) )
64 63 oveq1d 
 |-  ( ( 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 ) )
65 24 zred 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) e. RR )
66 65 20 resubcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) e. RR )
67 29 zred 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) e. RR )
68 67 26 resubcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) e. RR )
69 absreimsq 
 |-  ( ( ( ( |_ ` ( ( ( 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 ) ) )
70 66 68 69 syl2anc 
 |-  ( ( 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 ) ) )
71 64 70 eqtrd 
 |-  ( ( 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 ) ) )
72 66 resqcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ^ 2 ) e. RR )
73 68 resqcld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ^ 2 ) e. RR )
74 21 resqcli 
 |-  ( ( 1 / 2 ) ^ 2 ) e. RR
75 74 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( 1 / 2 ) ^ 2 ) e. RR )
76 21 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( 1 / 2 ) e. RR )
77 absresq 
 |-  ( ( ( |_ ` ( ( ( 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 ) )
78 66 77 syl 
 |-  ( ( 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 ) )
79 rddif 
 |-  ( ( ( Re ` y ) / r ) e. RR -> ( abs ` ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ) <_ ( 1 / 2 ) )
80 20 79 syl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( abs ` ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ) <_ ( 1 / 2 ) )
81 66 recnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) e. CC )
82 81 abscld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( abs ` ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ) e. RR )
83 81 absge0d 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> 0 <_ ( abs ` ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ) )
84 halfgt0 
 |-  0 < ( 1 / 2 )
85 21 84 elrpii 
 |-  ( 1 / 2 ) e. RR+
86 rpge0 
 |-  ( ( 1 / 2 ) e. RR+ -> 0 <_ ( 1 / 2 ) )
87 85 86 mp1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> 0 <_ ( 1 / 2 ) )
88 82 76 83 87 le2sqd 
 |-  ( ( 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 ) ) )
89 80 88 mpbid 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( abs ` ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ) ^ 2 ) <_ ( ( 1 / 2 ) ^ 2 ) )
90 78 89 eqbrtrrd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ^ 2 ) <_ ( ( 1 / 2 ) ^ 2 ) )
91 halfcn 
 |-  ( 1 / 2 ) e. CC
92 91 sqvali 
 |-  ( ( 1 / 2 ) ^ 2 ) = ( ( 1 / 2 ) x. ( 1 / 2 ) )
93 halflt1 
 |-  ( 1 / 2 ) < 1
94 21 39 21 84 ltmul1ii 
 |-  ( ( 1 / 2 ) < 1 <-> ( ( 1 / 2 ) x. ( 1 / 2 ) ) < ( 1 x. ( 1 / 2 ) ) )
95 93 94 mpbi 
 |-  ( ( 1 / 2 ) x. ( 1 / 2 ) ) < ( 1 x. ( 1 / 2 ) )
96 91 mullidi 
 |-  ( 1 x. ( 1 / 2 ) ) = ( 1 / 2 )
97 95 96 breqtri 
 |-  ( ( 1 / 2 ) x. ( 1 / 2 ) ) < ( 1 / 2 )
98 92 97 eqbrtri 
 |-  ( ( 1 / 2 ) ^ 2 ) < ( 1 / 2 )
99 98 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( 1 / 2 ) ^ 2 ) < ( 1 / 2 ) )
100 72 75 76 90 99 lelttrd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Re ` y ) / r ) ) ^ 2 ) < ( 1 / 2 ) )
101 absresq 
 |-  ( ( ( |_ ` ( ( ( 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 ) )
102 68 101 syl 
 |-  ( ( 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 ) )
103 rddif 
 |-  ( ( ( Im ` y ) / r ) e. RR -> ( abs ` ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ) <_ ( 1 / 2 ) )
104 26 103 syl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( abs ` ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ) <_ ( 1 / 2 ) )
105 68 recnd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) e. CC )
106 105 abscld 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( abs ` ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ) e. RR )
107 105 absge0d 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> 0 <_ ( abs ` ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ) )
108 106 76 107 87 le2sqd 
 |-  ( ( 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 ) ) )
109 104 108 mpbid 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( abs ` ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ) ^ 2 ) <_ ( ( 1 / 2 ) ^ 2 ) )
110 102 109 eqbrtrrd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ^ 2 ) <_ ( ( 1 / 2 ) ^ 2 ) )
111 73 75 76 110 99 lelttrd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( ( ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) - ( ( Im ` y ) / r ) ) ^ 2 ) < ( 1 / 2 ) )
112 72 73 40 100 111 lt2halvesd 
 |-  ( ( 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 )
113 71 112 eqbrtrd 
 |-  ( ( 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 )
114 sq1 
 |-  ( 1 ^ 2 ) = 1
115 113 114 breqtrrdi 
 |-  ( ( 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 ) )
116 37 absge0d 
 |-  ( ( 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 ) ) ) )
117 0le1 
 |-  0 <_ 1
118 117 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> 0 <_ 1 )
119 38 40 116 118 lt2sqd 
 |-  ( ( 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 ) ) )
120 115 119 mpbird 
 |-  ( ( 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 )
121 38 40 19 120 ltmul2dd 
 |-  ( ( 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 ) )
122 34 33 mulcld 
 |-  ( ( 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 )
123 eqid 
 |-  ( abs o. - ) = ( abs o. - )
124 123 cnmetdval 
 |-  ( ( ( 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 ) ) )
125 122 17 124 syl2anc 
 |-  ( ( 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 ) ) )
126 34 33 36 subdid 
 |-  ( ( 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 ) ) ) )
127 17 34 35 divcan2d 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( r x. ( y / r ) ) = y )
128 127 oveq2d 
 |-  ( ( 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 ) )
129 126 128 eqtrd 
 |-  ( ( 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 ) )
130 129 fveq2d 
 |-  ( ( 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 ) ) )
131 34 37 absmuld 
 |-  ( ( 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 ) ) ) ) )
132 130 131 eqtr3d 
 |-  ( ( 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 ) ) ) ) )
133 19 rpge0d 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> 0 <_ r )
134 52 133 absidd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( abs ` r ) = r )
135 134 oveq1d 
 |-  ( ( 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 ) ) ) ) )
136 125 132 135 3eqtrrd 
 |-  ( ( 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 ) )
137 34 mulridd 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( r x. 1 ) = r )
138 121 136 137 3brtr3d 
 |-  ( ( 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 )
139 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
140 139 a1i 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
141 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
142 141 ad2antrl 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> r e. RR* )
143 elbl2 
 |-  ( ( ( ( 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 ) )
144 140 142 122 17 143 syl22anc 
 |-  ( ( 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 ) )
145 138 144 mpbird 
 |-  ( ( 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 ) )
146 oveq2 
 |-  ( 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 ) ) ) ) ) ) )
147 146 oveq1d 
 |-  ( 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 ) )
148 147 eleq2d 
 |-  ( 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 ) ) )
149 148 rspcev 
 |-  ( ( ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) + ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) ) e. Z[i] /\ y e. ( ( r x. ( ( |_ ` ( ( ( Re ` y ) / r ) + ( 1 / 2 ) ) ) + ( _i x. ( |_ ` ( ( ( Im ` y ) / r ) + ( 1 / 2 ) ) ) ) ) ) ( ball ` ( abs o. - ) ) r ) ) -> E. z e. Z[i] y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) )
150 31 145 149 syl2anc 
 |-  ( ( D e. ( Bnd ` X ) /\ ( r e. RR+ /\ y e. X ) ) -> E. z e. Z[i] y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) )
151 150 expr 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> ( y e. X -> E. z e. Z[i] y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) ) )
152 eliun 
 |-  ( y e. U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) <-> E. x e. ran ( z e. Z[i] |-> ( r x. z ) ) y e. ( x ( ball ` ( abs o. - ) ) r ) )
153 ovex 
 |-  ( r x. z ) e. _V
154 153 rgenw 
 |-  A. z e. Z[i] ( r x. z ) e. _V
155 eqid 
 |-  ( z e. Z[i] |-> ( r x. z ) ) = ( z e. Z[i] |-> ( r x. z ) )
156 oveq1 
 |-  ( x = ( r x. z ) -> ( x ( ball ` ( abs o. - ) ) r ) = ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) )
157 156 eleq2d 
 |-  ( x = ( r x. z ) -> ( y e. ( x ( ball ` ( abs o. - ) ) r ) <-> y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) ) )
158 155 157 rexrnmptw 
 |-  ( A. z e. Z[i] ( r x. z ) e. _V -> ( E. x e. ran ( z e. Z[i] |-> ( r x. z ) ) y e. ( x ( ball ` ( abs o. - ) ) r ) <-> E. z e. Z[i] y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) ) )
159 154 158 ax-mp 
 |-  ( E. x e. ran ( z e. Z[i] |-> ( r x. z ) ) y e. ( x ( ball ` ( abs o. - ) ) r ) <-> E. z e. Z[i] y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) )
160 152 159 bitri 
 |-  ( y e. U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) <-> E. z e. Z[i] y e. ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) )
161 151 160 imbitrrdi 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> ( y e. X -> y e. U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) ) )
162 161 ssrdv 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> X C_ U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) )
163 simpl 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> D e. ( Bnd ` X ) )
164 0cn 
 |-  0 e. CC
165 1 ssbnd 
 |-  ( ( ( abs o. - ) e. ( Met ` CC ) /\ 0 e. CC ) -> ( D e. ( Bnd ` X ) <-> E. d e. RR X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) )
166 13 164 165 mp2an 
 |-  ( D e. ( Bnd ` X ) <-> E. d e. RR X C_ ( 0 ( ball ` ( abs o. - ) ) d ) )
167 163 166 sylib 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> E. d e. RR X C_ ( 0 ( ball ` ( abs o. - ) ) d ) )
168 fzfi 
 |-  ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) e. Fin
169 xpfi 
 |-  ( ( ( -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 )
170 168 168 169 mp2an 
 |-  ( ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) X. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) e. Fin
171 eqid 
 |-  ( 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 ) ) ) )
172 ovex 
 |-  ( r x. ( a + ( _i x. b ) ) ) e. _V
173 171 172 fnmpoi 
 |-  ( 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 ) ) )
174 dffn4 
 |-  ( ( 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 ) ) ) ) )
175 173 174 mpbi 
 |-  ( 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 ) ) ) )
176 fofi 
 |-  ( ( ( ( -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 )
177 170 175 176 mp2an 
 |-  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
178 155 153 elrnmpti 
 |-  ( x e. ran ( z e. Z[i] |-> ( r x. z ) ) <-> E. z e. Z[i] x = ( r x. z ) )
179 elgz 
 |-  ( z e. Z[i] <-> ( z e. CC /\ ( Re ` z ) e. ZZ /\ ( Im ` z ) e. ZZ ) )
180 179 simp2bi 
 |-  ( z e. Z[i] -> ( Re ` z ) e. ZZ )
181 180 ad2antlr 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Re ` z ) e. ZZ )
182 181 zcnd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Re ` z ) e. CC )
183 182 abscld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( Re ` z ) ) e. RR )
184 5 ad2antlr 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> z e. CC )
185 184 abscld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` z ) e. RR )
186 simpllr 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> r e. RR+ )
187 186 adantr 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> r e. RR+ )
188 187 rpred 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> r e. RR )
189 simplrl 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> d e. RR )
190 189 adantr 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> d e. RR )
191 188 190 readdcld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( r + d ) e. RR )
192 191 187 rerpdivcld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( r + d ) / r ) e. RR )
193 192 flcld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( |_ ` ( ( r + d ) / r ) ) e. ZZ )
194 193 peano2zd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. ZZ )
195 194 zred 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. RR )
196 absrele 
 |-  ( z e. CC -> ( abs ` ( Re ` z ) ) <_ ( abs ` z ) )
197 184 196 syl 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( Re ` z ) ) <_ ( abs ` z ) )
198 187 rpcnd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> r e. CC )
199 198 184 absmuld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( r x. z ) ) = ( ( abs ` r ) x. ( abs ` z ) ) )
200 187 rpge0d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> 0 <_ r )
201 188 200 absidd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` r ) = r )
202 201 oveq1d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( abs ` r ) x. ( abs ` z ) ) = ( r x. ( abs ` z ) ) )
203 199 202 eqtrd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( r x. z ) ) = ( r x. ( abs ` z ) ) )
204 simplrr 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> X C_ ( 0 ( ball ` ( abs o. - ) ) d ) )
205 sslin 
 |-  ( 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 ) ) )
206 204 205 syl 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[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 ) ) )
207 139 a1i 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( abs o. - ) e. ( *Met ` CC ) )
208 7 adantlr 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( r x. z ) e. CC )
209 164 a1i 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> 0 e. CC )
210 186 rpxrd 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> r e. RR* )
211 189 rexrd 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> d e. RR* )
212 bldisj 
 |-  ( ( ( ( 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 ) ) = (/) )
213 212 3exp2 
 |-  ( ( ( 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 ) ) = (/) ) ) ) )
214 213 imp32 
 |-  ( ( ( ( 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 ) ) = (/) ) )
215 207 208 209 210 211 214 syl32anc 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( ( r +e d ) <_ ( ( r x. z ) ( abs o. - ) 0 ) -> ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i ( 0 ( ball ` ( abs o. - ) ) d ) ) = (/) ) )
216 sseq0 
 |-  ( ( ( ( ( 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 ) = (/) )
217 206 215 216 syl6an 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( ( r +e d ) <_ ( ( r x. z ) ( abs o. - ) 0 ) -> ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) = (/) ) )
218 217 necon3ad 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> -. ( r +e d ) <_ ( ( r x. z ) ( abs o. - ) 0 ) ) )
219 218 imp 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> -. ( r +e d ) <_ ( ( r x. z ) ( abs o. - ) 0 ) )
220 rexadd 
 |-  ( ( r e. RR /\ d e. RR ) -> ( r +e d ) = ( r + d ) )
221 188 190 220 syl2anc 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( r +e d ) = ( r + d ) )
222 208 adantr 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( r x. z ) e. CC )
223 123 cnmetdval 
 |-  ( ( ( r x. z ) e. CC /\ 0 e. CC ) -> ( ( r x. z ) ( abs o. - ) 0 ) = ( abs ` ( ( r x. z ) - 0 ) ) )
224 222 164 223 sylancl 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( r x. z ) ( abs o. - ) 0 ) = ( abs ` ( ( r x. z ) - 0 ) ) )
225 222 subid1d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( r x. z ) - 0 ) = ( r x. z ) )
226 225 fveq2d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( ( r x. z ) - 0 ) ) = ( abs ` ( r x. z ) ) )
227 224 226 eqtrd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( r x. z ) ( abs o. - ) 0 ) = ( abs ` ( r x. z ) ) )
228 221 227 breq12d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[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 ) ) ) )
229 219 228 mtbid 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> -. ( r + d ) <_ ( abs ` ( r x. z ) ) )
230 222 abscld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( r x. z ) ) e. RR )
231 230 191 ltnled 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( abs ` ( r x. z ) ) < ( r + d ) <-> -. ( r + d ) <_ ( abs ` ( r x. z ) ) ) )
232 229 231 mpbird 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( r x. z ) ) < ( r + d ) )
233 203 232 eqbrtrrd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( r x. ( abs ` z ) ) < ( r + d ) )
234 185 191 187 ltmuldiv2d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( r x. ( abs ` z ) ) < ( r + d ) <-> ( abs ` z ) < ( ( r + d ) / r ) ) )
235 233 234 mpbid 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` z ) < ( ( r + d ) / r ) )
236 flltp1 
 |-  ( ( ( r + d ) / r ) e. RR -> ( ( r + d ) / r ) < ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) )
237 192 236 syl 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( r + d ) / r ) < ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) )
238 185 192 195 235 237 lttrd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` z ) < ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) )
239 185 195 238 ltled 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) )
240 183 185 195 197 239 letrd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( Re ` z ) ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) )
241 181 zred 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Re ` z ) e. RR )
242 241 195 absled 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( abs ` ( Re ` z ) ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <-> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Re ` z ) /\ ( Re ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) )
243 240 242 mpbid 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Re ` z ) /\ ( Re ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) )
244 194 znegcld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. ZZ )
245 elfz 
 |-  ( ( ( Re ` z ) e. ZZ /\ -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. ZZ /\ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. ZZ ) -> ( ( Re ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) <-> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Re ` z ) /\ ( Re ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) )
246 181 244 194 245 syl3anc 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( Re ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) <-> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Re ` z ) /\ ( Re ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) )
247 243 246 mpbird 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Re ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) )
248 179 simp3bi 
 |-  ( z e. Z[i] -> ( Im ` z ) e. ZZ )
249 248 ad2antlr 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Im ` z ) e. ZZ )
250 249 zcnd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Im ` z ) e. CC )
251 250 abscld 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( Im ` z ) ) e. RR )
252 absimle 
 |-  ( z e. CC -> ( abs ` ( Im ` z ) ) <_ ( abs ` z ) )
253 184 252 syl 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( Im ` z ) ) <_ ( abs ` z ) )
254 251 185 195 253 239 letrd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( abs ` ( Im ` z ) ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) )
255 249 zred 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Im ` z ) e. RR )
256 255 195 absled 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( abs ` ( Im ` z ) ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <-> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Im ` z ) /\ ( Im ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) )
257 254 256 mpbid 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Im ` z ) /\ ( Im ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) )
258 elfz 
 |-  ( ( ( Im ` z ) e. ZZ /\ -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. ZZ /\ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) e. ZZ ) -> ( ( Im ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) <-> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Im ` z ) /\ ( Im ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) )
259 249 244 194 258 syl3anc 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( ( Im ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) <-> ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) <_ ( Im ` z ) /\ ( Im ` z ) <_ ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ) )
260 257 259 mpbird 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( Im ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) )
261 184 replimd 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> z = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
262 261 oveq2d 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> ( r x. z ) = ( r x. ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) ) )
263 oveq1 
 |-  ( a = ( Re ` z ) -> ( a + ( _i x. b ) ) = ( ( Re ` z ) + ( _i x. b ) ) )
264 263 oveq2d 
 |-  ( a = ( Re ` z ) -> ( r x. ( a + ( _i x. b ) ) ) = ( r x. ( ( Re ` z ) + ( _i x. b ) ) ) )
265 264 eqeq2d 
 |-  ( a = ( Re ` z ) -> ( ( r x. z ) = ( r x. ( a + ( _i x. b ) ) ) <-> ( r x. z ) = ( r x. ( ( Re ` z ) + ( _i x. b ) ) ) ) )
266 oveq2 
 |-  ( b = ( Im ` z ) -> ( _i x. b ) = ( _i x. ( Im ` z ) ) )
267 266 oveq2d 
 |-  ( b = ( Im ` z ) -> ( ( Re ` z ) + ( _i x. b ) ) = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
268 267 oveq2d 
 |-  ( b = ( Im ` z ) -> ( r x. ( ( Re ` z ) + ( _i x. b ) ) ) = ( r x. ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) ) )
269 268 eqeq2d 
 |-  ( b = ( Im ` z ) -> ( ( r x. z ) = ( r x. ( ( Re ` z ) + ( _i x. b ) ) ) <-> ( r x. z ) = ( r x. ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) ) ) )
270 265 269 rspc2ev 
 |-  ( ( ( Re ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) /\ ( Im ` z ) e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) /\ ( r x. z ) = ( r x. ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) ) ) -> E. a e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) E. b e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ( r x. z ) = ( r x. ( a + ( _i x. b ) ) ) )
271 247 260 262 270 syl3anc 
 |-  ( ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) /\ ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> E. a e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) E. b e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ( r x. z ) = ( r x. ( a + ( _i x. b ) ) ) )
272 271 ex 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> E. a e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) E. b e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ( r x. z ) = ( r x. ( a + ( _i x. b ) ) ) ) )
273 171 172 elrnmpo 
 |-  ( ( r x. z ) e. 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. a e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) E. b e. ( -u ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ... ( ( |_ ` ( ( r + d ) / r ) ) + 1 ) ) ( r x. z ) = ( r x. ( a + ( _i x. b ) ) ) )
274 272 273 imbitrrdi 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> ( r x. z ) e. 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 ) ) ) ) ) )
275 156 ineq1d 
 |-  ( x = ( r x. z ) -> ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) = ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) )
276 275 neeq1d 
 |-  ( x = ( r x. z ) -> ( ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) <-> ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) )
277 eleq1 
 |-  ( x = ( r x. z ) -> ( x e. 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 ) ) ) ) <-> ( r x. z ) e. 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 ) ) ) ) ) )
278 276 277 imbi12d 
 |-  ( x = ( r x. z ) -> ( ( ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> x e. 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 ) ) ) ) ) <-> ( ( ( ( r x. z ) ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> ( r x. z ) e. 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 ) ) ) ) ) ) )
279 274 278 syl5ibrcom 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ z e. Z[i] ) -> ( x = ( r x. z ) -> ( ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> x e. 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 ) ) ) ) ) ) )
280 279 rexlimdva 
 |-  ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) -> ( E. z e. Z[i] x = ( r x. z ) -> ( ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> x e. 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 ) ) ) ) ) ) )
281 178 280 biimtrid 
 |-  ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) -> ( x e. ran ( z e. Z[i] |-> ( r x. z ) ) -> ( ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) -> x e. 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 ) ) ) ) ) ) )
282 281 3imp 
 |-  ( ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) /\ x e. ran ( z e. Z[i] |-> ( r x. z ) ) /\ ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) ) -> x e. 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 ) ) ) ) )
283 282 rabssdv 
 |-  ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) -> { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } C_ 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 ) ) ) ) )
284 ssfi 
 |-  ( ( 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 /\ { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } C_ 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 ) ) ) ) ) -> { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin )
285 177 283 284 sylancr 
 |-  ( ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) /\ ( d e. RR /\ X C_ ( 0 ( ball ` ( abs o. - ) ) d ) ) ) -> { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin )
286 167 285 rexlimddv 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin )
287 iuneq1 
 |-  ( y = ran ( z e. Z[i] |-> ( r x. z ) ) -> U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) = U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) )
288 287 sseq2d 
 |-  ( y = ran ( z e. Z[i] |-> ( r x. z ) ) -> ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) <-> X C_ U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) ) )
289 rabeq 
 |-  ( y = ran ( z e. Z[i] |-> ( r x. z ) ) -> { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } = { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } )
290 289 eleq1d 
 |-  ( y = ran ( z e. Z[i] |-> ( r x. z ) ) -> ( { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin <-> { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) )
291 288 290 anbi12d 
 |-  ( y = ran ( z e. Z[i] |-> ( r x. z ) ) -> ( ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) <-> ( X C_ U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) ) )
292 291 rspcev 
 |-  ( ( ran ( z e. Z[i] |-> ( r x. z ) ) e. ~P CC /\ ( X C_ U_ x e. ran ( z e. Z[i] |-> ( r x. z ) ) ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. ran ( z e. Z[i] |-> ( r x. z ) ) | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) ) -> E. y e. ~P CC ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) )
293 12 162 286 292 syl12anc 
 |-  ( ( D e. ( Bnd ` X ) /\ r e. RR+ ) -> E. y e. ~P CC ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) )
294 293 ralrimiva 
 |-  ( D e. ( Bnd ` X ) -> A. r e. RR+ E. y e. ~P CC ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) )
295 1 sstotbnd3 
 |-  ( ( ( abs o. - ) e. ( Met ` CC ) /\ X C_ CC ) -> ( D e. ( TotBnd ` X ) <-> A. r e. RR+ E. y e. ~P CC ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) ) )
296 13 15 295 sylancr 
 |-  ( D e. ( Bnd ` X ) -> ( D e. ( TotBnd ` X ) <-> A. r e. RR+ E. y e. ~P CC ( X C_ U_ x e. y ( x ( ball ` ( abs o. - ) ) r ) /\ { x e. y | ( ( x ( ball ` ( abs o. - ) ) r ) i^i X ) =/= (/) } e. Fin ) ) )
297 294 296 mpbird 
 |-  ( D e. ( Bnd ` X ) -> D e. ( TotBnd ` X ) )
298 2 297 impbii 
 |-  ( D e. ( TotBnd ` X ) <-> D e. ( Bnd ` X ) )