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

Theorem cntotbnd 37782
Description: A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
Hypothesis
Ref Expression
cntotbnd.d 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))
Assertion
Ref Expression
cntotbnd (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))

Proof of Theorem cntotbnd
Dummy variables 𝑎 𝑏 𝑑 𝑟 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 totbndbnd 37775 . 2 (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋))
2 rpcn 13042 . . . . . . . . . 10 (𝑟 ∈ ℝ+𝑟 ∈ ℂ)
32adantl 481 . . . . . . . . 9 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℂ)
4 gzcn 16965 . . . . . . . . 9 (𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ)
5 mulcl 11236 . . . . . . . . 9 ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ)
63, 4, 5syl2an 596 . . . . . . . 8 (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
76fmpttd 7134 . . . . . . 7 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)):ℤ[i]⟶ℂ)
87frnd 6744 . . . . . 6 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
9 cnex 11233 . . . . . . 7 ℂ ∈ V
109elpw2 5339 . . . . . 6 (ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ↔ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
118, 10sylibr 234 . . . . 5 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ)
12 cnmet 24807 . . . . . . . . . . . . . . . . 17 (abs ∘ − ) ∈ (Met‘ℂ)
13 cntotbnd.d . . . . . . . . . . . . . . . . . 18 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))
1413bnd2lem 37777 . . . . . . . . . . . . . . . . 17 (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ)
1512, 14mpan 690 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ)
1615sselda 3994 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦𝑋) → 𝑦 ∈ ℂ)
1716adantrl 716 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑦 ∈ ℂ)
1817recld 15229 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (ℜ‘𝑦) ∈ ℝ)
19 simprl 771 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑟 ∈ ℝ+)
2018, 19rerpdivcld 13105 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ)
21 halfre 12477 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
22 readdcl 11235 . . . . . . . . . . . 12 ((((ℜ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
2320, 21, 22sylancl 586 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
2423flcld 13834 . . . . . . . . . 10 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
2517imcld 15230 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (ℑ‘𝑦) ∈ ℝ)
2625, 19rerpdivcld 13105 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ)
27 readdcl 11235 . . . . . . . . . . . 12 ((((ℑ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
2826, 21, 27sylancl 586 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
2928flcld 13834 . . . . . . . . . 10 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
30 gzreim 16972 . . . . . . . . . 10 (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
3124, 29, 30syl2anc 584 . . . . . . . . 9 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
32 gzcn 16965 . . . . . . . . . . . . . . 15 (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℂ)
3331, 32syl 17 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℂ)
3419rpcnd 13076 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑟 ∈ ℂ)
3519rpne0d 13079 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑟 ≠ 0)
3617, 34, 35divcld 12040 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑦 / 𝑟) ∈ ℂ)
3733, 36subcld 11617 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ)
3837abscld 15471 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ)
39 1re 11258 . . . . . . . . . . . . 13 1 ∈ ℝ
4039a1i 11 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 1 ∈ ℝ)
4124zcnd 12720 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
42 ax-icn 11211 . . . . . . . . . . . . . . . . . . . . 21 i ∈ ℂ
4329zcnd 12720 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
44 mulcl 11236 . . . . . . . . . . . . . . . . . . . . 21 ((i ∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
4542, 43, 44sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
4620recnd 11286 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ)
4726recnd 11286 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ)
48 mulcl 11236 . . . . . . . . . . . . . . . . . . . . 21 ((i ∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
4942, 47, 48sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
5041, 45, 46, 49addsub4d 11664 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
5136replimd 15232 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))))
5219rpred 13074 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑟 ∈ ℝ)
5352, 17, 35redivd 15264 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟))
5452, 17, 35imdivd 15265 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟))
5554oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟)))
5653, 55oveq12d 7448 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
5751, 56eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
5857oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))))
5942a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → i ∈ ℂ)
6059, 43, 47subdid 11716 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟))))
6160oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
6250, 58, 613eqtr4d 2784 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))
6362fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))))
6463oveq1d 7445 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2))
6524zred 12719 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
6665, 20resubcld 11688 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ)
6729zred 12719 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
6867, 26resubcld 11688 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ)
69 absreimsq 15327 . . . . . . . . . . . . . . . . 17 ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧ ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
7066, 68, 69syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
7164, 70eqtrd 2774 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
7266resqcld 14161 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ)
7368resqcld 14161 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ)
7421resqcli 14221 . . . . . . . . . . . . . . . . . 18 ((1 / 2)↑2) ∈ ℝ
7574a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((1 / 2)↑2) ∈ ℝ)
7621a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (1 / 2) ∈ ℝ)
77 absresq 15337 . . . . . . . . . . . . . . . . . . 19 (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2))
7866, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2))
79 rddif 15375 . . . . . . . . . . . . . . . . . . . 20 (((ℜ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
8020, 79syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
8166recnd 11286 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ)
8281abscld 15471 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ)
8381absge0d 15479 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 0 ≤ (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))))
84 halfgt0 12479 . . . . . . . . . . . . . . . . . . . . . 22 0 < (1 / 2)
8521, 84elrpii 13034 . . . . . . . . . . . . . . . . . . . . 21 (1 / 2) ∈ ℝ+
86 rpge0 13045 . . . . . . . . . . . . . . . . . . . . 21 ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
8785, 86mp1i 13 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 0 ≤ (1 / 2))
8882, 76, 83, 87le2sqd 14292 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔ ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2)))
8980, 88mpbid 232 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2))
9078, 89eqbrtrrd 5171 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
91 halfcn 12478 . . . . . . . . . . . . . . . . . . . 20 (1 / 2) ∈ ℂ
9291sqvali 14215 . . . . . . . . . . . . . . . . . . 19 ((1 / 2)↑2) = ((1 / 2) · (1 / 2))
93 halflt1 12481 . . . . . . . . . . . . . . . . . . . . 21 (1 / 2) < 1
9421, 39, 21, 84ltmul1ii 12193 . . . . . . . . . . . . . . . . . . . . 21 ((1 / 2) < 1 ↔ ((1 / 2) · (1 / 2)) < (1 · (1 / 2)))
9593, 94mpbi 230 . . . . . . . . . . . . . . . . . . . 20 ((1 / 2) · (1 / 2)) < (1 · (1 / 2))
9691mullidi 11263 . . . . . . . . . . . . . . . . . . . 20 (1 · (1 / 2)) = (1 / 2)
9795, 96breqtri 5172 . . . . . . . . . . . . . . . . . . 19 ((1 / 2) · (1 / 2)) < (1 / 2)
9892, 97eqbrtri 5168 . . . . . . . . . . . . . . . . . 18 ((1 / 2)↑2) < (1 / 2)
9998a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((1 / 2)↑2) < (1 / 2))
10072, 75, 76, 90, 99lelttrd 11416 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2))
101 absresq 15337 . . . . . . . . . . . . . . . . . . 19 (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))
10268, 101syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))
103 rddif 15375 . . . . . . . . . . . . . . . . . . . 20 (((ℑ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
10426, 103syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
10568recnd 11286 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
106105abscld 15471 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ)
107105absge0d 15479 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 0 ≤ (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))
108106, 76, 107, 87le2sqd 14292 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔ ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2)))
109104, 108mpbid 232 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2))
110102, 109eqbrtrrd 5171 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
11173, 75, 76, 110, 99lelttrd 11416 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2))
11272, 73, 40, 100, 111lt2halvesd 12511 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1)
11371, 112eqbrtrd 5169 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1)
114 sq1 14230 . . . . . . . . . . . . . 14 (1↑2) = 1
115113, 114breqtrrdi 5189 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2))
11637absge0d 15479 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 0 ≤ (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))
117 0le1 11783 . . . . . . . . . . . . . . 15 0 ≤ 1
118117a1i 11 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 0 ≤ 1)
11938, 40, 116, 118lt2sqd 14291 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1 ↔ ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2)))
120115, 119mpbird 257 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1)
12138, 40, 19, 120ltmul2dd 13130 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1))
12234, 33mulcld 11278 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ)
123 eqid 2734 . . . . . . . . . . . . . 14 (abs ∘ − ) = (abs ∘ − )
124123cnmetdval 24806 . . . . . . . . . . . . 13 (((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
125122, 17, 124syl2anc 584 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
12634, 33, 36subdid 11716 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))))
12717, 34, 35divcan2d 12042 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦)
128127oveq2d 7446 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
129126, 128eqtrd 2774 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
130129fveq2d 6910 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
13134, 37absmuld 15489 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
132130, 131eqtr3d 2776 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
13319rpge0d 13078 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 0 ≤ 𝑟)
13452, 133absidd 15457 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs‘𝑟) = 𝑟)
135134oveq1d 7445 . . . . . . . . . . . 12 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
136125, 132, 1353eqtrrd 2779 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦))
13734mulridd 11275 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑟 · 1) = 𝑟)
138121, 136, 1373brtr3d 5178 . . . . . . . . . 10 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)
139 cnxmet 24808 . . . . . . . . . . . 12 (abs ∘ − ) ∈ (∞Met‘ℂ)
140139a1i 11 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
141 rpxr 13041 . . . . . . . . . . . 12 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
142141ad2antrl 728 . . . . . . . . . . 11 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑟 ∈ ℝ*)
143 elbl2 24415 . . . . . . . . . . 11 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟) ↔ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟))
144140, 142, 122, 17, 143syl22anc 839 . . . . . . . . . 10 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → (𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟) ↔ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟))
145138, 144mpbird 257 . . . . . . . . 9 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
146 oveq2 7438 . . . . . . . . . . . 12 (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))))
147146oveq1d 7445 . . . . . . . . . . 11 (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
148147eleq2d 2824 . . . . . . . . . 10 (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)))
149148rspcev 3621 . . . . . . . . 9 ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
15031, 145, 149syl2anc 584 . . . . . . . 8 ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+𝑦𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
151150expr 456 . . . . . . 7 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
152 eliun 4999 . . . . . . . 8 (𝑦 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
153 ovex 7463 . . . . . . . . . 10 (𝑟 · 𝑧) ∈ V
154153rgenw 3062 . . . . . . . . 9 𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V
155 eqid 2734 . . . . . . . . . 10 (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))
156 oveq1 7437 . . . . . . . . . . 11 (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
157156eleq2d 2824 . . . . . . . . . 10 (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
158155, 157rexrnmptw 7114 . . . . . . . . 9 (∀𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V → (∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
159154, 158ax-mp 5 . . . . . . . 8 (∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
160152, 159bitri 275 . . . . . . 7 (𝑦 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
161151, 160imbitrrdi 252 . . . . . 6 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦𝑋𝑦 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
162161ssrdv 4000 . . . . 5 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
163 simpl 482 . . . . . . 7 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Bnd‘𝑋))
164 0cn 11250 . . . . . . . 8 0 ∈ ℂ
16513ssbnd 37774 . . . . . . . 8 (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) → (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑)))
16612, 164, 165mp2an 692 . . . . . . 7 (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
167163, 166sylib 218 . . . . . 6 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
168 fzfi 14009 . . . . . . . . 9 (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin
169 xpfi 9355 . . . . . . . . 9 (((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) → ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin)
170168, 168, 169mp2an 692 . . . . . . . 8 ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin
171 eqid 2734 . . . . . . . . . 10 (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
172 ovex 7463 . . . . . . . . . 10 (𝑟 · (𝑎 + (i · 𝑏))) ∈ V
173171, 172fnmpoi 8093 . . . . . . . . 9 (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
174 dffn4 6826 . . . . . . . . 9 ((𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 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 · 𝑏)))))
175173, 174mpbi 230 . . . . . . . 8 (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
176 fofi 9348 . . . . . . . 8 ((((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 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)
177170, 175, 176mp2an 692 . . . . . . 7 ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin
178155, 153elrnmpti 5975 . . . . . . . . . 10 (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧))
179 elgz 16964 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧ (ℜ‘𝑧) ∈ ℤ ∧ (ℑ‘𝑧) ∈ ℤ))
180179simp2bi 1145 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℤ[i] → (ℜ‘𝑧) ∈ ℤ)
181180ad2antlr 727 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℤ)
182181zcnd 12720 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℂ)
183182abscld 15471 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ∈ ℝ)
1844ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ)
185184abscld 15471 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈ ℝ)
186 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ+)
187186adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ+)
188187rpred 13074 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ)
189 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ)
190189adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ)
191188, 190readdcld 11287 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ)
192191, 187rerpdivcld 13105 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ)
193192flcld 13834 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ)
194193peano2zd 12722 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
195194zred 12719 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ)
196 absrele 15343 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
197184, 196syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
198187rpcnd 13076 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ)
199198, 184absmuld 15489 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧)))
200187rpge0d 13078 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟)
201188, 200absidd 15457 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟)
202201oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧)))
203199, 202eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧)))
204 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
205 sslin 4250 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
207139a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (abs ∘ − ) ∈ (∞Met‘ℂ))
2086adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
209164a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 0 ∈ ℂ)
210186rpxrd 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ*)
211189rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ*)
212 bldisj 24423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ*𝑑 ∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅)
2132123exp2 1353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → (𝑟 ∈ ℝ* → (𝑑 ∈ ℝ* → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))))
214213imp32 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ*𝑑 ∈ ℝ*)) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
215207, 208, 209, 210, 211, 214syl32anc 1377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
216 sseq0 4408 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅)
217206, 215, 216syl6an 684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅))
218217necon3ad 2950 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)))
219218imp 406 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))
220 rexadd 13270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
221188, 190, 220syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
222208adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ)
223123cnmetdval 24806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
224222, 164, 223sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
225222subid1d 11606 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧))
226225fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧)))
227224, 226eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧)))
228221, 227breq12d 5160 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) ↔ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
229219, 228mtbid 324 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))
230222abscld 15471 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ)
231230, 191ltnled 11405 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
232229, 231mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑))
233203, 232eqbrtrrd 5171 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑))
234185, 191, 187ltmuldiv2d 13122 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)))
235233, 234mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))
236 flltp1 13836 . . . . . . . . . . . . . . . . . . . . 21 (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
237192, 236syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
238185, 192, 195, 235, 237lttrd 11419 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
239185, 195, 238ltled 11406 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
240183, 185, 195, 197, 239letrd 11415 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
241181zred 12719 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℝ)
242241, 195absled 15465 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
243240, 242mpbid 232 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
244194znegcld 12721 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
245 elfz 13549 . . . . . . . . . . . . . . . . 17 (((ℜ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
246181, 244, 194, 245syl3anc 1370 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
247243, 246mpbird 257 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
248179simp3bi 1146 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℤ[i] → (ℑ‘𝑧) ∈ ℤ)
249248ad2antlr 727 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℤ)
250249zcnd 12720 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℂ)
251250abscld 15471 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ∈ ℝ)
252 absimle 15344 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧))
253184, 252syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧))
254251, 185, 195, 253, 239letrd 11415 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
255249zred 12719 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℝ)
256255, 195absled 15465 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
257254, 256mpbid 232 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
258 elfz 13549 . . . . . . . . . . . . . . . . 17 (((ℑ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
259249, 244, 194, 258syl3anc 1370 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
260257, 259mpbird 257 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
261184replimd 15232 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
262261oveq2d 7446 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
263 oveq1 7437 . . . . . . . . . . . . . . . . . 18 (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏)))
264263oveq2d 7446 . . . . . . . . . . . . . . . . 17 (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))
265264eqeq2d 2745 . . . . . . . . . . . . . . . 16 (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))))
266 oveq2 7438 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i · (ℑ‘𝑧)))
267266oveq2d 7446 . . . . . . . . . . . . . . . . . 18 (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
268267oveq2d 7446 . . . . . . . . . . . . . . . . 17 (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
269268eqeq2d 2745 . . . . . . . . . . . . . . . 16 (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))))
270265, 269rspc2ev 3634 . . . . . . . . . . . . . . 15 (((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
271247, 260, 262, 270syl3anc 1370 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
272271ex 412 . . . . . . . . . . . . 13 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))))
273171, 172elrnmpo 7568 . . . . . . . . . . . . 13 ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
274272, 273imbitrrdi 252 . . . . . . . . . . . 12 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
275156ineq1d 4226 . . . . . . . . . . . . . 14 (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
276275neeq1d 2997 . . . . . . . . . . . . 13 (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅))
277 eleq1 2826 . . . . . . . . . . . . 13 (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
278276, 277imbi12d 344 . . . . . . . . . . . 12 (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
279274, 278syl5ibrcom 247 . . . . . . . . . . 11 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
280279rexlimdva 3152 . . . . . . . . . 10 (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
281178, 280biimtrid 242 . . . . . . . . 9 (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
2822813imp 1110 . . . . . . . 8 ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
283282rabssdv 4084 . . . . . . 7 (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
284 ssfi 9211 . . . . . . 7 ((ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
285177, 283, 284sylancr 587 . . . . . 6 (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
286167, 285rexlimddv 3158 . . . . 5 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
287 iuneq1 5012 . . . . . . . 8 (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
288287sseq2d 4027 . . . . . . 7 (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
289 rabeq 3447 . . . . . . . 8 (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅})
290289eleq1d 2823 . . . . . . 7 (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
291288, 290anbi12d 632 . . . . . 6 (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
292291rspcev 3621 . . . . 5 ((ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ∧ (𝑋 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
29311, 162, 286, 292syl12anc 837 . . . 4 ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
294293ralrimiva 3143 . . 3 (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+𝑦 ∈ 𝒫 ℂ(𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
29513sstotbnd3 37762 . . . 4 (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+𝑦 ∈ 𝒫 ℂ(𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
29612, 15, 295sylancr 587 . . 3 (𝐷 ∈ (Bnd‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+𝑦 ∈ 𝒫 ℂ(𝑋 𝑥𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
297294, 296mpbird 257 . 2 (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋))
2981, 297impbii 209 1 (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604   ciun 4995   class class class wbr 5147  cmpt 5230   × cxp 5686  ran crn 5689  cres 5690  ccom 5692   Fn wfn 6557  ontowfo 6560  cfv 6562  (class class class)co 7430  cmpo 7432  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153  ici 11154   + caddc 11155   · cmul 11157  *cxr 11291   < clt 11292  cle 11293  cmin 11489  -cneg 11490   / cdiv 11917  2c2 12318  cz 12610  +crp 13031   +𝑒 cxad 13149  ...cfz 13543  cfl 13826  cexp 14098  cre 15132  cim 15133  abscabs 15269  ℤ[i]cgz 16962  ∞Metcxmet 21366  Metcmet 21367  ballcbl 21368  TotBndctotbnd 37752  Bndcbnd 37753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-ec 8745  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-fz 13544  df-fl 13828  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-gz 16963  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-totbnd 37754  df-bnd 37765
This theorem is referenced by:  cnpwstotbnd  37783
  Copyright terms: Public domain W3C validator