Theorem cntotbnd 37756

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 37749	. 2 ⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋))
2		rpcn 13067	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℂ)
3	2	adantl 481	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℂ)
4		gzcn 16979	. . . . . . . . 9 ⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ)
5		mulcl 11268	. . . . . . . . 9 ⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ)
6	3, 4, 5	syl2an 595	. . . . . . . 8 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
7	6	fmpttd 7149	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)):ℤ[i]⟶ℂ)
8	7	frnd 6755	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
9		cnex 11265	. . . . . . 7 ⊢ ℂ ∈ V
10	9	elpw2 5352	. . . . . 6 ⊢ (ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ↔ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
11	8, 10	sylibr 234	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ)
12		cnmet 24813	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (Met‘ℂ)
13		cntotbnd.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))
14	13	bnd2lem 37751	. . . . . . . . . . . . . . . . 17 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ)
15	12, 14	mpan 689	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ)
16	15	sselda 4008	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ)
17	16	adantrl 715	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ)
18	17	recld 15243	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ)
19		simprl 770	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ+)
20	18, 19	rerpdivcld 13130	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ)
21		halfre 12507	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
22		readdcl 11267	. . . . . . . . . . . 12 ⊢ ((((ℜ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
23	20, 21, 22	sylancl 585	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
24	23	flcld 13849	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
25	17	imcld 15244	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ)
26	25, 19	rerpdivcld 13130	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ)
27		readdcl 11267	. . . . . . . . . . . 12 ⊢ ((((ℑ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
28	26, 21, 27	sylancl 585	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
29	28	flcld 13849	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
30		gzreim 16986	. . . . . . . . . 10 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
31	24, 29, 30	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
32		gzcn 16979	. . . . . . . . . . . . . . 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 13101	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ)
35	19	rpne0d 13104	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0)
36	17, 34, 35	divcld 12070	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ)
37	33, 36	subcld 11647	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ)
38	37	abscld 15485	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ)
39		1re 11290	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ)
41	24	zcnd 12748	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
42		ax-icn 11243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ i ∈ ℂ
43	29	zcnd 12748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
44		mulcl 11268	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
45	42, 43, 44	sylancr 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
46	20	recnd 11318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ)
47	26	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ)
48		mulcl 11268	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
49	42, 47, 48	sylancr 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
50	41, 45, 46, 49	addsub4d 11694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
51	36	replimd 15246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))))
52	19	rpred 13099	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ)
53	52, 17, 35	redivd 15278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟))
54	52, 17, 35	imdivd 15279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟))
55	54	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟)))
56	53, 55	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
57	51, 56	eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
58	57	oveq2d 7464	. . . . . . . . . . . . . . . . . . 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 11746	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟))))
61	60	oveq2d 7464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
62	50, 58, 61	3eqtr4d 2790	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))
63	62	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))))
64	63	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2))
65	24	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
66	65, 20	resubcld 11718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ)
67	29	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
68	67, 26	resubcld 11718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ)
69		absreimsq 15341	. . . . . . . . . . . . . . . . 17 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧ ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
70	66, 68, 69	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
71	64, 70	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
72	66	resqcld 14175	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ)
73	68	resqcld 14175	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ)
74	21	resqcli 14235	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) ∈ ℝ
75	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈ ℝ)
76	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈ ℝ)
77		absresq 15351	. . . . . . . . . . . . . . . . . . 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 15389	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℜ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
80	20, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
81	66	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ)
82	81	abscld 15485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ)
83	81	absge0d 15493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))))
84		halfgt0 12509	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < (1 / 2)
85	21, 84	elrpii 13060	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) ∈ ℝ+
86		rpge0 13070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
87	85, 86	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2))
88	82, 76, 83, 87	le2sqd 14306	. . . . . . . . . . . . . . . . . . 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 5190	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
91		halfcn 12508	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 2) ∈ ℂ
92	91	sqvali 14229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2)↑2) = ((1 / 2) · (1 / 2))
93		halflt1 12511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) < 1
94	21, 39, 21, 84	ltmul1ii 12223	. . . . . . . . . . . . . . . . . . . . 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 11295	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 · (1 / 2)) = (1 / 2)
97	95, 96	breqtri 5191	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) · (1 / 2)) < (1 / 2)
98	92, 97	eqbrtri 5187	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) < (1 / 2)
99	98	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 / 2))
100	72, 75, 76, 90, 99	lelttrd 11448	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2))
101		absresq 15351	. . . . . . . . . . . . . . . . . . 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 15389	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℑ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
104	26, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
105	68	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
106	105	abscld 15485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ)
107	105	absge0d 15493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))
108	106, 76, 107, 87	le2sqd 14306	. . . . . . . . . . . . . . . . . . 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 5190	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
111	73, 75, 76, 110, 99	lelttrd 11448	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2))
112	72, 73, 40, 100, 111	lt2halvesd 12541	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1)
113	71, 112	eqbrtrd 5188	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1)
114		sq1 14244	. . . . . . . . . . . . . 14 ⊢ (1↑2) = 1
115	113, 114	breqtrrdi 5208	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2))
116	37	absge0d 15493	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))
117		0le1 11813	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
118	117	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1)
119	38, 40, 116, 118	lt2sqd 14305	. . . . . . . . . . . . 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 13155	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1))
122	34, 33	mulcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ)
123		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) = (abs ∘ − )
124	123	cnmetdval 24812	. . . . . . . . . . . . 13 ⊢ (((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
125	122, 17, 124	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
126	34, 33, 36	subdid 11746	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))))
127	17, 34, 35	divcan2d 12072	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦)
128	127	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
129	126, 128	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
130	129	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
131	34, 37	absmuld 15503	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
132	130, 131	eqtr3d 2782	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
133	19	rpge0d 13103	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟)
134	52, 133	absidd 15471	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟)
135	134	oveq1d 7463	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
136	125, 132, 135	3eqtrrd 2785	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦))
137	34	mulridd 11307	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟)
138	121, 136, 137	3brtr3d 5197	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)
139		cnxmet 24814	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
140	139	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
141		rpxr 13066	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
142	141	ad2antrl 727	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ*)
143		elbl2 24421	. . . . . . . . . . 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 7456	. . . . . . . . . . . 12 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))))
147	146	oveq1d 7463	. . . . . . . . . . 11 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
148	147	eleq2d 2830	. . . . . . . . . 10 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)))
149	148	rspcev 3635	. . . . . . . . 9 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
150	31, 145, 149	syl2anc 583	. . . . . . . 8 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
151	150	expr 456	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
152		eliun 5019	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
153		ovex 7481	. . . . . . . . . 10 ⊢ (𝑟 · 𝑧) ∈ V
154	153	rgenw 3071	. . . . . . . . 9 ⊢ ∀𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V
155		eqid 2740	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))
156		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
157	156	eleq2d 2830	. . . . . . . . . 10 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
158	155, 157	rexrnmptw 7129	. . . . . . . . 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 4014	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
163		simpl 482	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Bnd‘𝑋))
164		0cn 11282	. . . . . . . 8 ⊢ 0 ∈ ℂ
165	13	ssbnd 37748	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) → (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑)))
166	12, 164, 165	mp2an 691	. . . . . . 7 ⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
167	163, 166	sylib 218	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
168		fzfi 14023	. . . . . . . . 9 ⊢ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin
169		xpfi 9386	. . . . . . . . 9 ⊢ (((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) → ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin)
170	168, 168, 169	mp2an 691	. . . . . . . 8 ⊢ ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin
171		eqid 2740	. . . . . . . . . 10 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
172		ovex 7481	. . . . . . . . . 10 ⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V
173	171, 172	fnmpoi 8111	. . . . . . . . 9 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
174		dffn4 6840	. . . . . . . . 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 9379	. . . . . . . 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 691	. . . . . . 7 ⊢ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin
178	155, 153	elrnmpti 5985	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧))
179		elgz 16978	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧ (ℜ‘𝑧) ∈ ℤ ∧ (ℑ‘𝑧) ∈ ℤ))
180	179	simp2bi 1146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℜ‘𝑧) ∈ ℤ)
181	180	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℤ)
182	181	zcnd 12748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℂ)
183	182	abscld 15485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ∈ ℝ)
184	4	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ)
185	184	abscld 15485	. . . . . . . . . . . . . . . . . 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 13099	. . . . . . . . . . . . . . . . . . . . . . 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 11319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ)
192	191, 187	rerpdivcld 13130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ)
193	192	flcld 13849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ)
194	193	peano2zd 12750	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
195	194	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ)
196		absrele 15357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
197	184, 196	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
198	187	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ)
199	198, 184	absmuld 15503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧)))
200	187	rpge0d 13103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟)
201	188, 200	absidd 15471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟)
202	201	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧)))
203	199, 202	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧)))
204		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
205		sslin 4264	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
209	164	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 0 ∈ ℂ)
210	186	rpxrd 13100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ*)
211	189	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ*)
212		bldisj 24429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅)
213	212	3exp2 1354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1378	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
216		sseq0 4426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅)
217	206, 215, 216	syl6an 683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅))
218	217	necon3ad 2959	. . . . . . . . . . . . . . . . . . . . . . . . 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 13294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
221	188, 190, 220	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
222	208	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ)
223	123	cnmetdval 24812	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
224	222, 164, 223	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
225	222	subid1d 11636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧))
226	225	fveq2d 6924	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧)))
227	224, 226	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧)))
228	221, 227	breq12d 5179	. . . . . . . . . . . . . . . . . . . . . . . 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 15485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ)
231	230, 191	ltnled 11437	. . . . . . . . . . . . . . . . . . . . . . 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 5190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑))
234	185, 191, 187	ltmuldiv2d 13147	. . . . . . . . . . . . . . . . . . . . 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 13851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
237	192, 236	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
238	185, 192, 195, 235, 237	lttrd 11451	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
239	185, 195, 238	ltled 11438	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
240	183, 185, 195, 197, 239	letrd 11447	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
241	181	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℝ)
242	241, 195	absled 15479	. . . . . . . . . . . . . . . . 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 12749	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
245		elfz 13573	. . . . . . . . . . . . . . . . 17 ⊢ (((ℜ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
246	181, 244, 194, 245	syl3anc 1371	. . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℤ)
250	249	zcnd 12748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℂ)
251	250	abscld 15485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ∈ ℝ)
252		absimle 15358	. . . . . . . . . . . . . . . . . . 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 11447	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
255	249	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℝ)
256	255, 195	absled 15479	. . . . . . . . . . . . . . . . 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 13573	. . . . . . . . . . . . . . . . 17 ⊢ (((ℑ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
259	249, 244, 194, 258	syl3anc 1371	. . . . . . . . . . . . . . . 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 15246	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
262	261	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
263		oveq1 7455	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏)))
264	263	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))
265	264	eqeq2d 2751	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))))
266		oveq2 7456	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i · (ℑ‘𝑧)))
267	266	oveq2d 7464	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
268	267	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
269	268	eqeq2d 2751	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))))
270	265, 269	rspc2ev 3648	. . . . . . . . . . . . . . 15 ⊢ (((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
271	247, 260, 262, 270	syl3anc 1371	. . . . . . . . . . . . . 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 7586	. . . . . . . . . . . . 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 4240	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
276	275	neeq1d 3006	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅))
277		eleq1 2832	. . . . . . . . . . . . 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 3161	. . . . . . . . . 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 1111	. . . . . . . 8 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
283	282	rabssdv 4098	. . . . . . 7 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
284		ssfi 9240	. . . . . . 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 586	. . . . . 6 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
286	167, 285	rexlimddv 3167	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
287		iuneq1 5031	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
288	287	sseq2d 4041	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
289		rabeq 3458	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅})
290	289	eleq1d 2829	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
291	288, 290	anbi12d 631	. . . . . 6 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
292	291	rspcev 3635	. . . . 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 3152	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
295	13	sstotbnd3 37736	. . . 4 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
296	12, 15, 295	sylancr 586	. . 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 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622  ∪ ciun 5015   class class class wbr 5166   ↦ cmpt 5249   × cxp 5698  ran crn 5701   ↾ cres 5702   ∘ ccom 5704   Fn wfn 6568  –onto→wfo 6571  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  Fincfn 9003  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185  ici 11186   + caddc 11187   · cmul 11189  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325   − cmin 11520  -cneg 11521   / cdiv 11947  2c2 12348  ℤcz 12639  ℝ⁺crp 13057   +_𝑒 cxad 13173  ...cfz 13567  ⌊cfl 13841  ↑cexp 14112  ℜcre 15146  ℑcim 15147  abscabs 15283  ℤ[i]cgz 16976  ∞Metcxmet 21372  Metcmet 21373  ballcbl 21374  TotBndctotbnd 37726  Bndcbnd 37727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-ec 8765  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-fz 13568  df-fl 13843  df-seq 14053  df-exp 14113  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-gz 16977  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-totbnd 37728  df-bnd 37739

This theorem is referenced by:  cnpwstotbnd  37757