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 0cn ⊢ 0 ∈ ℂ
164 1 ssbnd ⊢ ( ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ 0 ∈ ℂ ) → ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ↔ ∃ 𝑑 ∈ ℝ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
165 13 163 164 mp2an ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ↔ ∃ 𝑑 ∈ ℝ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
166 165 birani ⊢ ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
167 fzfi ⊢ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∈ Fin
168 xpfi ⊢ ( ( ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∈ Fin ∧ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∈ Fin ) → ( ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) × ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) ∈ Fin )
169 167 167 168 mp2an ⊢ ( ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) × ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) ∈ Fin
170 eqid ⊢ ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) = ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) )
171 ovex ⊢ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ∈ V
172 170 171 fnmpoi ⊢ ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) Fn ( ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) × ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) )
173 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 · 𝑏 ) ) ) ) )
174 172 173 mpbi ⊢ ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) : ( ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) × ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) –onto→ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) )
175 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 )
176 169 174 175 mp2an ⊢ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ∈ Fin
177 155 153 elrnmpti ⊢ ( 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ↔ ∃ 𝑧 ∈ ℤ[i] 𝑥 = ( 𝑟 · 𝑧 ) )
178 elgz ⊢ ( 𝑧 ∈ ℤ[i] ↔ ( 𝑧 ∈ ℂ ∧ ( ℜ ‘ 𝑧 ) ∈ ℤ ∧ ( ℑ ‘ 𝑧 ) ∈ ℤ ) )
179 178 simp2bi ⊢ ( 𝑧 ∈ ℤ[i] → ( ℜ ‘ 𝑧 ) ∈ ℤ )
180 179 ad2antlr ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℜ ‘ 𝑧 ) ∈ ℤ )
181 180 zcnd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℜ ‘ 𝑧 ) ∈ ℂ )
182 181 abscld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ℜ ‘ 𝑧 ) ) ∈ ℝ )
183 5 ad2antlr ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑧 ∈ ℂ )
184 183 abscld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ 𝑧 ) ∈ ℝ )
185 simpllr ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → 𝑟 ∈ ℝ+ )
186 185 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑟 ∈ ℝ+ )
187 186 rpred ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑟 ∈ ℝ )
188 simplrl ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → 𝑑 ∈ ℝ )
189 188 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑑 ∈ ℝ )
190 187 189 readdcld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( 𝑟 + 𝑑 ) ∈ ℝ )
191 190 186 rerpdivcld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 + 𝑑 ) / 𝑟 ) ∈ ℝ )
192 191 flcld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) ∈ ℤ )
193 192 peano2zd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℤ )
194 193 zred ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℝ )
195 absrele ⊢ ( 𝑧 ∈ ℂ → ( abs ‘ ( ℜ ‘ 𝑧 ) ) ≤ ( abs ‘ 𝑧 ) )
196 183 195 syl ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ℜ ‘ 𝑧 ) ) ≤ ( abs ‘ 𝑧 ) )
197 186 rpcnd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑟 ∈ ℂ )
198 197 183 absmuld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( 𝑟 · 𝑧 ) ) = ( ( abs ‘ 𝑟 ) · ( abs ‘ 𝑧 ) ) )
199 186 rpge0d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 0 ≤ 𝑟 )
200 187 199 absidd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ 𝑟 ) = 𝑟 )
201 200 oveq1d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( abs ‘ 𝑟 ) · ( abs ‘ 𝑧 ) ) = ( 𝑟 · ( abs ‘ 𝑧 ) ) )
202 198 201 eqtrd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( 𝑟 · 𝑧 ) ) = ( 𝑟 · ( abs ‘ 𝑧 ) ) )
203 simplrr ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
204 sslin ⊢ ( 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ⊆ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
205 203 204 syl ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ⊆ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
206 139 a1i ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
207 7 adantlr ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( 𝑟 · 𝑧 ) ∈ ℂ )
208 163 a1i ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → 0 ∈ ℂ )
209 185 rpxrd ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → 𝑟 ∈ ℝ* )
210 188 rexrd ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → 𝑑 ∈ ℝ* )
211 bldisj ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝑟 · 𝑧 ) ∈ ℂ ∧ 0 ∈ ℂ ) ∧ ( 𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ* ∧ ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) ) ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) = ∅ )
212 211 3exp2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝑟 · 𝑧 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑟 ∈ ℝ* → ( 𝑑 ∈ ℝ* → ( ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) = ∅ ) ) ) )
213 212 imp32 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝑟 · 𝑧 ) ∈ ℂ ∧ 0 ∈ ℂ ) ∧ ( 𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ* ) ) → ( ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) = ∅ ) )
214 206 207 208 209 210 213 syl32anc ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) = ∅ ) )
215 sseq0 ⊢ ( ( ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ⊆ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) = ∅ ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) = ∅ )
216 205 214 215 syl6an ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) → ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) = ∅ ) )
217 216 necon3ad ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → ¬ ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) ) )
218 217 imp ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ¬ ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) )
219 rexadd ⊢ ( ( 𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑟 +𝑒 𝑑 ) = ( 𝑟 + 𝑑 ) )
220 187 189 219 syl2anc ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( 𝑟 +𝑒 𝑑 ) = ( 𝑟 + 𝑑 ) )
221 207 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( 𝑟 · 𝑧 ) ∈ ℂ )
222 123 cnmetdval ⊢ ( ( ( 𝑟 · 𝑧 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) = ( abs ‘ ( ( 𝑟 · 𝑧 ) − 0 ) ) )
223 221 163 222 sylancl ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) = ( abs ‘ ( ( 𝑟 · 𝑧 ) − 0 ) ) )
224 221 subid1d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 · 𝑧 ) − 0 ) = ( 𝑟 · 𝑧 ) )
225 224 fveq2d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ( 𝑟 · 𝑧 ) − 0 ) ) = ( abs ‘ ( 𝑟 · 𝑧 ) ) )
226 223 225 eqtrd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑟 · 𝑧 ) ) )
227 220 226 breq12d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 +𝑒 𝑑 ) ≤ ( ( 𝑟 · 𝑧 ) ( abs ∘ − ) 0 ) ↔ ( 𝑟 + 𝑑 ) ≤ ( abs ‘ ( 𝑟 · 𝑧 ) ) ) )
228 218 227 mtbid ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ¬ ( 𝑟 + 𝑑 ) ≤ ( abs ‘ ( 𝑟 · 𝑧 ) ) )
229 221 abscld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( 𝑟 · 𝑧 ) ) ∈ ℝ )
230 229 190 ltnled ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( abs ‘ ( 𝑟 · 𝑧 ) ) < ( 𝑟 + 𝑑 ) ↔ ¬ ( 𝑟 + 𝑑 ) ≤ ( abs ‘ ( 𝑟 · 𝑧 ) ) ) )
231 228 230 mpbird ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( 𝑟 · 𝑧 ) ) < ( 𝑟 + 𝑑 ) )
232 202 231 eqbrtrrd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( 𝑟 · ( abs ‘ 𝑧 ) ) < ( 𝑟 + 𝑑 ) )
233 184 190 186 ltmuldiv2d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 · ( abs ‘ 𝑧 ) ) < ( 𝑟 + 𝑑 ) ↔ ( abs ‘ 𝑧 ) < ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) )
234 232 233 mpbid ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ 𝑧 ) < ( ( 𝑟 + 𝑑 ) / 𝑟 ) )
235 flltp1 ⊢ ( ( ( 𝑟 + 𝑑 ) / 𝑟 ) ∈ ℝ → ( ( 𝑟 + 𝑑 ) / 𝑟 ) < ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) )
236 191 235 syl ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( 𝑟 + 𝑑 ) / 𝑟 ) < ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) )
237 184 191 194 234 236 lttrd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ 𝑧 ) < ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) )
238 184 194 237 ltled ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) )
239 182 184 194 196 238 letrd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ℜ ‘ 𝑧 ) ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) )
240 180 zred ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℜ ‘ 𝑧 ) ∈ ℝ )
241 240 194 absled ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( abs ‘ ( ℜ ‘ 𝑧 ) ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ↔ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℜ ‘ 𝑧 ) ∧ ( ℜ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) )
242 239 241 mpbid ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℜ ‘ 𝑧 ) ∧ ( ℜ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) )
243 193 znegcld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℤ )
244 elfz ⊢ ( ( ( ℜ ‘ 𝑧 ) ∈ ℤ ∧ - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℤ ∧ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℤ ) → ( ( ℜ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↔ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℜ ‘ 𝑧 ) ∧ ( ℜ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) )
245 180 243 193 244 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( ℜ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↔ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℜ ‘ 𝑧 ) ∧ ( ℜ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) )
246 242 245 mpbird ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℜ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) )
247 178 simp3bi ⊢ ( 𝑧 ∈ ℤ[i] → ( ℑ ‘ 𝑧 ) ∈ ℤ )
248 247 ad2antlr ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℑ ‘ 𝑧 ) ∈ ℤ )
249 248 zcnd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℑ ‘ 𝑧 ) ∈ ℂ )
250 249 abscld ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ℑ ‘ 𝑧 ) ) ∈ ℝ )
251 absimle ⊢ ( 𝑧 ∈ ℂ → ( abs ‘ ( ℑ ‘ 𝑧 ) ) ≤ ( abs ‘ 𝑧 ) )
252 183 251 syl ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ℑ ‘ 𝑧 ) ) ≤ ( abs ‘ 𝑧 ) )
253 250 184 194 252 238 letrd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( abs ‘ ( ℑ ‘ 𝑧 ) ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) )
254 248 zred ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℑ ‘ 𝑧 ) ∈ ℝ )
255 254 194 absled ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( abs ‘ ( ℑ ‘ 𝑧 ) ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ↔ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℑ ‘ 𝑧 ) ∧ ( ℑ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) )
256 253 255 mpbid ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℑ ‘ 𝑧 ) ∧ ( ℑ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) )
257 elfz ⊢ ( ( ( ℑ ‘ 𝑧 ) ∈ ℤ ∧ - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℤ ∧ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ∈ ℤ ) → ( ( ℑ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↔ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℑ ‘ 𝑧 ) ∧ ( ℑ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) )
258 248 243 193 257 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ( ℑ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↔ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ≤ ( ℑ ‘ 𝑧 ) ∧ ( ℑ ‘ 𝑧 ) ≤ ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ) )
259 256 258 mpbird ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( ℑ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) )
260 183 replimd ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑧 = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
261 260 oveq2d ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ( 𝑟 · 𝑧 ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) ) )
262 oveq1 ⊢ ( 𝑎 = ( ℜ ‘ 𝑧 ) → ( 𝑎 + ( i · 𝑏 ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · 𝑏 ) ) )
263 262 oveq2d ⊢ ( 𝑎 = ( ℜ ‘ 𝑧 ) → ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · 𝑏 ) ) ) )
264 263 eqeq2d ⊢ ( 𝑎 = ( ℜ ‘ 𝑧 ) → ( ( 𝑟 · 𝑧 ) = ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ↔ ( 𝑟 · 𝑧 ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · 𝑏 ) ) ) ) )
265 oveq2 ⊢ ( 𝑏 = ( ℑ ‘ 𝑧 ) → ( i · 𝑏 ) = ( i · ( ℑ ‘ 𝑧 ) ) )
266 265 oveq2d ⊢ ( 𝑏 = ( ℑ ‘ 𝑧 ) → ( ( ℜ ‘ 𝑧 ) + ( i · 𝑏 ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
267 266 oveq2d ⊢ ( 𝑏 = ( ℑ ‘ 𝑧 ) → ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · 𝑏 ) ) ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) ) )
268 267 eqeq2d ⊢ ( 𝑏 = ( ℑ ‘ 𝑧 ) → ( ( 𝑟 · 𝑧 ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · 𝑏 ) ) ) ↔ ( 𝑟 · 𝑧 ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) ) ) )
269 264 268 rspc2ev ⊢ ( ( ( ℜ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∧ ( ℑ ‘ 𝑧 ) ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∧ ( 𝑟 · 𝑧 ) = ( 𝑟 · ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) ) ) → ∃ 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∃ 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ( 𝑟 · 𝑧 ) = ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) )
270 246 259 261 269 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) ∧ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → ∃ 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∃ 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ( 𝑟 · 𝑧 ) = ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) )
271 270 ex ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → ∃ 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∃ 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ( 𝑟 · 𝑧 ) = ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) )
272 170 171 elrnmpo ⊢ ( ( 𝑟 · 𝑧 ) ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ↔ ∃ 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ∃ 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ( 𝑟 · 𝑧 ) = ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) )
273 271 272 imbitrrdi ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → ( 𝑟 · 𝑧 ) ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) )
274 156 ineq1d ⊢ ( 𝑥 = ( 𝑟 · 𝑧 ) → ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) = ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) )
275 274 neeq1d ⊢ ( 𝑥 = ( 𝑟 · 𝑧 ) → ( ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ↔ ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) )
276 eleq1 ⊢ ( 𝑥 = ( 𝑟 · 𝑧 ) → ( 𝑥 ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ↔ ( 𝑟 · 𝑧 ) ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) )
277 275 276 imbi12d ⊢ ( 𝑥 = ( 𝑟 · 𝑧 ) → ( ( ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → 𝑥 ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) ↔ ( ( ( ( 𝑟 · 𝑧 ) ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → ( 𝑟 · 𝑧 ) ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) ) )
278 273 277 syl5ibrcom ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑧 ∈ ℤ[i] ) → ( 𝑥 = ( 𝑟 · 𝑧 ) → ( ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → 𝑥 ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) ) )
279 278 rexlimdva ⊢ ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) → ( ∃ 𝑧 ∈ ℤ[i] 𝑥 = ( 𝑟 · 𝑧 ) → ( ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → 𝑥 ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) ) )
280 177 279 biimtrid ⊢ ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) → ( 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) → ( ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ → 𝑥 ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) ) )
281 280 3imp ⊢ ( ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) ∧ 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∧ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ ) → 𝑥 ∈ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) )
282 281 rabssdv ⊢ ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) → { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ⊆ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) )
283 ssfi ⊢ ( ( ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ∈ Fin ∧ { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ⊆ ran ( 𝑎 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) , 𝑏 ∈ ( - ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ... ( ( ⌊ ‘ ( ( 𝑟 + 𝑑 ) / 𝑟 ) ) + 1 ) ) ↦ ( 𝑟 · ( 𝑎 + ( i · 𝑏 ) ) ) ) ) → { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin )
284 176 282 283 sylancr ⊢ ( ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ ∧ 𝑋 ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) → { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin )
285 166 284 rexlimddv ⊢ ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin )
286 iuneq1 ⊢ ( 𝑦 = ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) → ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) = ∪ 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
287 286 sseq2d ⊢ ( 𝑦 = ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) → ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
288 rabeq ⊢ ( 𝑦 = ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) → { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } = { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } )
289 288 eleq1d ⊢ ( 𝑦 = ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) → ( { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ↔ { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) )
290 287 289 anbi12d ⊢ ( 𝑦 = ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) → ( ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ↔ ( 𝑋 ⊆ ∪ 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ) )
291 290 rspcev ⊢ ( ( ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∈ 𝒫 ℂ ∧ ( 𝑋 ⊆ ∪ 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ ran ( 𝑧 ∈ ℤ[i] ↦ ( 𝑟 · 𝑧 ) ) ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ) → ∃ 𝑦 ∈ 𝒫 ℂ ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) )
292 12 162 285 291 syl12anc ⊢ ( ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝒫 ℂ ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) )
293 292 ralrimiva ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑦 ∈ 𝒫 ℂ ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) )
294 1 sstotbnd3 ⊢ ( ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑦 ∈ 𝒫 ℂ ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ) )
295 13 15 294 sylancr ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑦 ∈ 𝒫 ℂ ( 𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ { 𝑥 ∈ 𝑦 ∣ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ) )
296 293 295 mpbird ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑋 ) → 𝐷 ∈ ( TotBnd ‘ 𝑋 ) )
297 2 296 impbii ⊢ ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝐷 ∈ ( Bnd ‘ 𝑋 ) )