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}={\left(\mathrm{abs}\circ -\right)↾}_{\left({X}×{X}\right)}$
Assertion cntotbnd ${⊢}{D}\in \mathrm{TotBnd}\left({X}\right)↔{D}\in \mathrm{Bnd}\left({X}\right)$

Proof

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