Theorem cntotbnd 37786

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.

Step	Hyp	Ref	Expression
1		totbndbnd 37779	. 2 ⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋))
2		rpcn 12904	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℂ)
3	2	adantl 481	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℂ)
4		gzcn 16844	. . . . . . . . 9 ⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ)
5		mulcl 11093	. . . . . . . . 9 ⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ)
6	3, 4, 5	syl2an 596	. . . . . . . 8 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
7	6	fmpttd 7049	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)):ℤ[i]⟶ℂ)
8	7	frnd 6660	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
9		cnex 11090	. . . . . . 7 ⊢ ℂ ∈ V
10	9	elpw2 5273	. . . . . 6 ⊢ (ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ↔ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
11	8, 10	sylibr 234	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ)
12		cnmet 24657	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (Met‘ℂ)
13		cntotbnd.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))
14	13	bnd2lem 37781	. . . . . . . . . . . . . . . . 17 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ)
15	12, 14	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ)
16	15	sselda 3935	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ)
17	16	adantrl 716	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ)
18	17	recld 15101	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ)
19		simprl 770	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ+)
20	18, 19	rerpdivcld 12968	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ)
21		halfre 12337	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
22		readdcl 11092	. . . . . . . . . . . 12 ⊢ ((((ℜ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
23	20, 21, 22	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
24	23	flcld 13702	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
25	17	imcld 15102	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ)
26	25, 19	rerpdivcld 12968	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ)
27		readdcl 11092	. . . . . . . . . . . 12 ⊢ ((((ℑ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
28	26, 21, 27	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
29	28	flcld 13702	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
30		gzreim 16851	. . . . . . . . . 10 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
31	24, 29, 30	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
32		gzcn 16844	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℂ)
33	31, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℂ)
34	19	rpcnd 12939	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ)
35	19	rpne0d 12942	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0)
36	17, 34, 35	divcld 11900	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ)
37	33, 36	subcld 11475	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ)
38	37	abscld 15346	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ)
39		1re 11115	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ)
41	24	zcnd 12581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
42		ax-icn 11068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ i ∈ ℂ
43	29	zcnd 12581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
44		mulcl 11093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
45	42, 43, 44	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
46	20	recnd 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ)
47	26	recnd 11143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ)
48		mulcl 11093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
49	42, 47, 48	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
50	41, 45, 46, 49	addsub4d 11522	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
51	36	replimd 15104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))))
52	19	rpred 12937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ)
53	52, 17, 35	redivd 15136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟))
54	52, 17, 35	imdivd 15137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟))
55	54	oveq2d 7365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟)))
56	53, 55	oveq12d 7367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
57	51, 56	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
58	57	oveq2d 7365	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))))
59	42	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → i ∈ ℂ)
60	59, 43, 47	subdid 11576	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟))))
61	60	oveq2d 7365	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
62	50, 58, 61	3eqtr4d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))
63	62	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))))
64	63	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2))
65	24	zred 12580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
66	65, 20	resubcld 11548	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ)
67	29	zred 12580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
68	67, 26	resubcld 11548	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ)
69		absreimsq 15199	. . . . . . . . . . . . . . . . 17 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧ ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
70	66, 68, 69	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
71	64, 70	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
72	66	resqcld 14032	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ)
73	68	resqcld 14032	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ)
74	21	resqcli 14093	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) ∈ ℝ
75	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈ ℝ)
76	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈ ℝ)
77		absresq 15209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2))
78	66, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2))
79		rddif 15248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℜ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
80	20, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
81	66	recnd 11143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ)
82	81	abscld 15346	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ)
83	81	absge0d 15354	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))))
84		halfgt0 12339	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < (1 / 2)
85	21, 84	elrpii 12896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) ∈ ℝ+
86		rpge0 12907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
87	85, 86	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2))
88	82, 76, 83, 87	le2sqd 14164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔ ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2)))
89	80, 88	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2))
90	78, 89	eqbrtrrd 5116	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
91		halfcn 12338	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 2) ∈ ℂ
92	91	sqvali 14087	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2)↑2) = ((1 / 2) · (1 / 2))
93		halflt1 12341	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) < 1
94	21, 39, 21, 84	ltmul1ii 12053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 / 2) < 1 ↔ ((1 / 2) · (1 / 2)) < (1 · (1 / 2)))
95	93, 94	mpbi 230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 / 2) · (1 / 2)) < (1 · (1 / 2))
96	91	mullidi 11120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 · (1 / 2)) = (1 / 2)
97	95, 96	breqtri 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) · (1 / 2)) < (1 / 2)
98	92, 97	eqbrtri 5113	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) < (1 / 2)
99	98	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 / 2))
100	72, 75, 76, 90, 99	lelttrd 11274	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2))
101		absresq 15209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))
102	68, 101	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))
103		rddif 15248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℑ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
104	26, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
105	68	recnd 11143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
106	105	abscld 15346	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ)
107	105	absge0d 15354	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))
108	106, 76, 107, 87	le2sqd 14164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔ ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2)))
109	104, 108	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2))
110	102, 109	eqbrtrrd 5116	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
111	73, 75, 76, 110, 99	lelttrd 11274	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2))
112	72, 73, 40, 100, 111	lt2halvesd 12372	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1)
113	71, 112	eqbrtrd 5114	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1)
114		sq1 14102	. . . . . . . . . . . . . 14 ⊢ (1↑2) = 1
115	113, 114	breqtrrdi 5134	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2))
116	37	absge0d 15354	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))
117		0le1 11643	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
118	117	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1)
119	38, 40, 116, 118	lt2sqd 14163	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1 ↔ ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2)))
120	115, 119	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1)
121	38, 40, 19, 120	ltmul2dd 12993	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1))
122	34, 33	mulcld 11135	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ)
123		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) = (abs ∘ − )
124	123	cnmetdval 24656	. . . . . . . . . . . . 13 ⊢ (((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
125	122, 17, 124	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
126	34, 33, 36	subdid 11576	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))))
127	17, 34, 35	divcan2d 11902	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦)
128	127	oveq2d 7365	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
129	126, 128	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
130	129	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
131	34, 37	absmuld 15364	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
132	130, 131	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
133	19	rpge0d 12941	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟)
134	52, 133	absidd 15330	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟)
135	134	oveq1d 7364	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
136	125, 132, 135	3eqtrrd 2769	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦))
137	34	mulridd 11132	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟)
138	121, 136, 137	3brtr3d 5123	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)
139		cnxmet 24658	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
140	139	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
141		rpxr 12903	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
142	141	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ*)
143		elbl2 24276	. . . . . . . . . . 11 ⊢ ((((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 838	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟) ↔ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟))
145	138, 144	mpbird 257	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
146		oveq2 7357	. . . . . . . . . . . 12 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))))
147	146	oveq1d 7364	. . . . . . . . . . 11 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
148	147	eleq2d 2814	. . . . . . . . . 10 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)))
149	148	rspcev 3577	. . . . . . . . 9 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
150	31, 145, 149	syl2anc 584	. . . . . . . 8 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
151	150	expr 456	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
152		eliun 4945	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
153		ovex 7382	. . . . . . . . . 10 ⊢ (𝑟 · 𝑧) ∈ V
154	153	rgenw 3048	. . . . . . . . 9 ⊢ ∀𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V
155		eqid 2729	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))
156		oveq1 7356	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
157	156	eleq2d 2814	. . . . . . . . . 10 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
158	155, 157	rexrnmptw 7029	. . . . . . . . 9 ⊢ (∀𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V → (∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
159	154, 158	ax-mp 5	. . . . . . . 8 ⊢ (∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
160	152, 159	bitri 275	. . . . . . 7 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
161	151, 160	imbitrrdi 252	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
162	161	ssrdv 3941	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
163		simpl 482	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Bnd‘𝑋))
164		0cn 11107	. . . . . . . 8 ⊢ 0 ∈ ℂ
165	13	ssbnd 37778	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) → (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑)))
166	12, 164, 165	mp2an 692	. . . . . . 7 ⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
167	163, 166	sylib 218	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
168		fzfi 13879	. . . . . . . . 9 ⊢ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin
169		xpfi 9209	. . . . . . . . 9 ⊢ (((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) → ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin)
170	168, 168, 169	mp2an 692	. . . . . . . 8 ⊢ ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin
171		eqid 2729	. . . . . . . . . 10 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
172		ovex 7382	. . . . . . . . . 10 ⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V
173	171, 172	fnmpoi 8005	. . . . . . . . 9 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
174		dffn4 6742	. . . . . . . . 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 · 𝑏)))))
175	173, 174	mpbi 230	. . . . . . . 8 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
176		fofi 9202	. . . . . . . 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)
177	170, 175, 176	mp2an 692	. . . . . . 7 ⊢ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin
178	155, 153	elrnmpti 5904	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧))
179		elgz 16843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧ (ℜ‘𝑧) ∈ ℤ ∧ (ℑ‘𝑧) ∈ ℤ))
180	179	simp2bi 1146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℜ‘𝑧) ∈ ℤ)
181	180	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℤ)
182	181	zcnd 12581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℂ)
183	182	abscld 15346	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ∈ ℝ)
184	4	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ)
185	184	abscld 15346	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈ ℝ)
186		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ+)
187	186	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ+)
188	187	rpred 12937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ)
189		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ)
190	189	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ)
191	188, 190	readdcld 11144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ)
192	191, 187	rerpdivcld 12968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ)
193	192	flcld 13702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ)
194	193	peano2zd 12583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
195	194	zred 12580	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ)
196		absrele 15215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
197	184, 196	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
198	187	rpcnd 12939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ)
199	198, 184	absmuld 15364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧)))
200	187	rpge0d 12941	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟)
201	188, 200	absidd 15330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟)
202	201	oveq1d 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧)))
203	199, 202	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧)))
204		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
205		sslin 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
207	139	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (abs ∘ − ) ∈ (∞Met‘ℂ))
208	6	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
209	164	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 0 ∈ ℂ)
210	186	rpxrd 12938	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ*)
211	189	rexrd 11165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ*)
212		bldisj 24284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅)
213	212	3exp2 1355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → (𝑟 ∈ ℝ* → (𝑑 ∈ ℝ* → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))))
214	213	imp32 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ*)) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
215	207, 208, 209, 210, 211, 214	syl32anc 1380	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
216		sseq0 4354	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅)
217	206, 215, 216	syl6an 684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅))
218	217	necon3ad 2938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)))
219	218	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))
220		rexadd 13134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
221	188, 190, 220	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
222	208	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ)
223	123	cnmetdval 24656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
224	222, 164, 223	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
225	222	subid1d 11464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧))
226	225	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧)))
227	224, 226	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧)))
228	221, 227	breq12d 5105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) ↔ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
229	219, 228	mtbid 324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))
230	222	abscld 15346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ)
231	230, 191	ltnled 11263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
232	229, 231	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑))
233	203, 232	eqbrtrrd 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑))
234	185, 191, 187	ltmuldiv2d 12985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)))
235	233, 234	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))
236		flltp1 13704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
237	192, 236	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
238	185, 192, 195, 235, 237	lttrd 11277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
239	185, 195, 238	ltled 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
240	183, 185, 195, 197, 239	letrd 11273	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
241	181	zred 12580	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℝ)
242	241, 195	absled 15340	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
243	240, 242	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
244	194	znegcld 12582	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
245		elfz 13416	. . . . . . . . . . . . . . . . 17 ⊢ (((ℜ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
246	181, 244, 194, 245	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
247	243, 246	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
248	179	simp3bi 1147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℑ‘𝑧) ∈ ℤ)
249	248	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℤ)
250	249	zcnd 12581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℂ)
251	250	abscld 15346	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ∈ ℝ)
252		absimle 15216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧))
253	184, 252	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧))
254	251, 185, 195, 253, 239	letrd 11273	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
255	249	zred 12580	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℝ)
256	255, 195	absled 15340	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
257	254, 256	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
258		elfz 13416	. . . . . . . . . . . . . . . . 17 ⊢ (((ℑ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
259	249, 244, 194, 258	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
260	257, 259	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
261	184	replimd 15104	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
262	261	oveq2d 7365	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
263		oveq1 7356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏)))
264	263	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))
265	264	eqeq2d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))))
266		oveq2 7357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i · (ℑ‘𝑧)))
267	266	oveq2d 7365	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
268	267	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
269	268	eqeq2d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))))
270	265, 269	rspc2ev 3590	. . . . . . . . . . . . . . 15 ⊢ (((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
271	247, 260, 262, 270	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
272	271	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))))
273	171, 172	elrnmpo 7485	. . . . . . . . . . . . 13 ⊢ ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
274	272, 273	imbitrrdi 252	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
275	156	ineq1d 4170	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
276	275	neeq1d 2984	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅))
277		eleq1 2816	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
278	276, 277	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
279	274, 278	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
280	279	rexlimdva 3130	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
281	178, 280	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
282	281	3imp 1110	. . . . . . . 8 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
283	282	rabssdv 4026	. . . . . . 7 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
284		ssfi 9087	. . . . . . 7 ⊢ ((ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
285	177, 283, 284	sylancr 587	. . . . . 6 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
286	167, 285	rexlimddv 3136	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
287		iuneq1 4958	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
288	287	sseq2d 3968	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
289		rabeq 3409	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅})
290	289	eleq1d 2813	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
291	288, 290	anbi12d 632	. . . . . 6 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
292	291	rspcev 3577	. . . . 5 ⊢ ((ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ∧ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
293	11, 162, 286, 292	syl12anc 836	. . . 4 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
294	293	ralrimiva 3121	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
295	13	sstotbnd3 37766	. . . 4 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
296	12, 15, 295	sylancr 587	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
297	294, 296	mpbird 257	. 2 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋))
298	1, 297	impbii 209	1 ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3394  Vcvv 3436   ∩ cin 3902   ⊆ wss 3903  ∅c0 4284  𝒫 cpw 4551  ∪ ciun 4941   class class class wbr 5092   ↦ cmpt 5173   × cxp 5617  ran crn 5620   ↾ cres 5621   ∘ ccom 5623   Fn wfn 6477  –onto→wfo 6480  ‘cfv 6482  (class class class)co 7349   ∈ cmpo 7351  Fincfn 8872  ℂcc 11007  ℝcr 11008  0cc0 11009  1c1 11010  ici 11011   + caddc 11012   · cmul 11014  ℝ^*cxr 11148   < clt 11149   ≤ cle 11150   − cmin 11347  -cneg 11348   / cdiv 11777  2c2 12183  ℤcz 12471  ℝ⁺crp 12893   +_𝑒 cxad 13012  ...cfz 13410  ⌊cfl 13694  ↑cexp 13968  ℜcre 15004  ℑcim 15005  abscabs 15141  ℤ[i]cgz 16841  ∞Metcxmet 21246  Metcmet 21247  ballcbl 21248  TotBndctotbnd 37756  Bndcbnd 37757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-ec 8627  df-map 8755  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-sup 9332  df-inf 9333  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-n0 12385  df-z 12472  df-uz 12736  df-rp 12894  df-xneg 13014  df-xadd 13015  df-xmul 13016  df-fz 13411  df-fl 13696  df-seq 13909  df-exp 13969  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-gz 16842  df-psmet 21253  df-xmet 21254  df-met 21255  df-bl 21256  df-totbnd 37758  df-bnd 37769

This theorem is referenced by:  cnpwstotbnd  37787