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 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( 𝑋 × 𝑋 ) )
Assertion cntotbnd ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝐷 ∈ ( Bnd ‘ 𝑋 ) )

Proof

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