Theorem cntotbnd 38335

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 38328	. 2 ⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋))
2		rpcn 13027	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℂ)
3	2	adantl 486	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℂ)
4		gzcn 16992	. . . . . . . . 9 ⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ)
5		mulcl 11184	. . . . . . . . 9 ⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ)
6	3, 4, 5	syl2an 607	. . . . . . . 8 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
7	6	fmpttd 7111	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)):ℤ[i]⟶ℂ)
8	7	frnd 6715	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
9		cnex 11181	. . . . . . 7 ⊢ ℂ ∈ V
10	9	elpw2 5305	. . . . . 6 ⊢ (ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ↔ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
11	8, 10	sylibr 237	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ)
12		cnmet 24897	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (Met‘ℂ)
13		cntotbnd.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))
14	13	bnd2lem 38330	. . . . . . . . . . . . . . . . 17 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ)
15	12, 14	mpan 702	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ)
16	15	sselda 3945	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ)
17	16	adantrl 728	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ)
18	17	recld 15245	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ)
19		simprl 782	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ+)
20	18, 19	rerpdivcld 13091	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ)
21		halfre 12457	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
22		readdcl 11183	. . . . . . . . . . . 12 ⊢ ((((ℜ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
23	20, 21, 22	sylancl 597	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
24	23	flcld 13831	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
25	17	imcld 15246	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ)
26	25, 19	rerpdivcld 13091	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ)
27		readdcl 11183	. . . . . . . . . . . 12 ⊢ ((((ℑ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
28	26, 21, 27	sylancl 597	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
29	28	flcld 13831	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
30		gzreim 16999	. . . . . . . . . 10 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
31	24, 29, 30	syl2anc 595	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
32		gzcn 16992	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℂ)
33	31, 32	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℂ)
34	19	rpcnd 13062	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ)
35	19	rpne0d 13065	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0)
36	17, 34, 35	divcld 11991	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ)
37	33, 36	subcld 11569	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ)
38	37	abscld 15490	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ)
39		1re 11208	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ)
41	24	zcnd 12701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
42		ax-icn 11159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ i ∈ ℂ
43	29	zcnd 12701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
44		mulcl 11184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
45	42, 43, 44	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
46	20	recnd 11237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ)
47	26	recnd 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ)
48		mulcl 11184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
49	42, 47, 48	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
50	41, 45, 46, 49	addsub4d 11616	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
51	36	replimd 15248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))))
52	19	rpred 13060	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ)
53	52, 17, 35	redivd 15280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟))
54	52, 17, 35	imdivd 15281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟))
55	54	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟)))
56	53, 55	oveq12d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
57	51, 56	eqtrd 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
58	57	oveq2d 7427	. . . . . . . . . . . . . . . . . . 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 11670	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟))))
61	60	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
62	50, 58, 61	3eqtr4d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))
63	62	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))))
64	63	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2))
65	24	zred 12700	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
66	65, 20	resubcld 11642	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ)
67	29	zred 12700	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
68	67, 26	resubcld 11642	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ)
69		absreimsq 15343	. . . . . . . . . . . . . . . . 17 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧ ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
70	66, 68, 69	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
71	64, 70	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
72	66	resqcld 14161	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ)
73	68	resqcld 14161	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ)
74	21	resqcli 14222	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) ∈ ℝ
75	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈ ℝ)
76	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈ ℝ)
77		absresq 15353	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2))
78	66, 77	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2))
79		rddif 15392	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℜ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
80	20, 79	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
81	66	recnd 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ)
82	81	abscld 15490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ)
83	81	absge0d 15498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))))
84		halfgt0 12459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < (1 / 2)
85	21, 84	elrpii 13019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) ∈ ℝ+
86		rpge0 13030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
87	85, 86	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2))
88	82, 76, 83, 87	le2sqd 14293	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔ ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2)))
89	80, 88	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2))
90	78, 89	eqbrtrrd 5139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
91		halfcn 12458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 2) ∈ ℂ
92	91	sqvali 14216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2)↑2) = ((1 / 2) · (1 / 2))
93		halflt1 12461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) < 1
94	21, 39, 21, 84	ltmul1ii 12143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 / 2) < 1 ↔ ((1 / 2) · (1 / 2)) < (1 · (1 / 2)))
95	93, 94	mpbi 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 / 2) · (1 / 2)) < (1 · (1 / 2))
96	91	mullidi 11214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 · (1 / 2)) = (1 / 2)
97	95, 96	breqtri 5140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) · (1 / 2)) < (1 / 2)
98	92, 97	eqbrtri 5136	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) < (1 / 2)
99	98	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 / 2))
100	72, 75, 76, 90, 99	lelttrd 11368	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2))
101		absresq 15353	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))
102	68, 101	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) = (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))
103		rddif 15392	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℑ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
104	26, 103	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
105	68	recnd 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
106	105	abscld 15490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ)
107	105	absge0d 15498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))
108	106, 76, 107, 87	le2sqd 14293	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔ ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2)))
109	104, 108	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 / 2)↑2))
110	102, 109	eqbrtrrd 5139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
111	73, 75, 76, 110, 99	lelttrd 11368	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2))
112	72, 73, 40, 100, 111	lt2halvesd 12492	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1)
113	71, 112	eqbrtrd 5137	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1)
114		sq1 14231	. . . . . . . . . . . . . 14 ⊢ (1↑2) = 1
115	113, 114	breqtrrdi 5157	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2))
116	37	absge0d 15498	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))
117		0le1 11737	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
118	117	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1)
119	38, 40, 116, 118	lt2sqd 14292	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1 ↔ ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2)))
120	115, 119	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1)
121	38, 40, 19, 120	ltmul2dd 13116	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1))
122	34, 33	mulcld 11229	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ)
123		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) = (abs ∘ − )
124	123	cnmetdval 24896	. . . . . . . . . . . . 13 ⊢ (((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
125	122, 17, 124	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
126	34, 33, 36	subdid 11670	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))))
127	17, 34, 35	divcan2d 11993	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦)
128	127	oveq2d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
129	126, 128	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
130	129	fveq2d 6886	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
131	34, 37	absmuld 15508	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
132	130, 131	eqtr3d 2806	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
133	19	rpge0d 13064	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟)
134	52, 133	absidd 15474	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟)
135	134	oveq1d 7426	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
136	125, 132, 135	3eqtrrd 2809	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦))
137	34	mulridd 11226	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟)
138	121, 136, 137	3brtr3d 5146	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)
139		cnxmet 24898	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
140	139	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
141		rpxr 13026	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
142	141	ad2antrl 740	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ*)
143		elbl2 24516	. . . . . . . . . . 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 851	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟) ↔ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟))
145	138, 144	mpbird 260	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
146		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))))
147	146	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
148	147	eleq2d 2855	. . . . . . . . . 10 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)))
149	148	rspcev 3590	. . . . . . . . 9 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
150	31, 145, 149	syl2anc 595	. . . . . . . 8 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
151	150	expr 461	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
152		eliun 4964	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
153		ovex 7444	. . . . . . . . . 10 ⊢ (𝑟 · 𝑧) ∈ V
154	153	rgenw 3089	. . . . . . . . 9 ⊢ ∀𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V
155		eqid 2769	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))
156		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
157	156	eleq2d 2855	. . . . . . . . . 10 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
158	155, 157	rexrnmptw 7091	. . . . . . . . 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 278	. . . . . . 7 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
161	151, 160	imbitrrdi 255	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
162	161	ssrdv 3951	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
163		0cn 11198	. . . . . . . 8 ⊢ 0 ∈ ℂ
164	13	ssbnd 38327	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) → (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑)))
165	12, 163, 164	mp2an 704	. . . . . . 7 ⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
166	165	birani 508	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
167		fzfi 14008	. . . . . . . . 9 ⊢ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin
168		xpfi 9279	. . . . . . . . 9 ⊢ (((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) → ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin)
169	167, 167, 168	mp2an 704	. . . . . . . 8 ⊢ ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin
170		eqid 2769	. . . . . . . . . 10 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
171		ovex 7444	. . . . . . . . . 10 ⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V
172	170, 171	fnmpoi 8067	. . . . . . . . 9 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
173		dffn4 6799	. . . . . . . . 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 · 𝑏)))))
174	172, 173	mpbi 233	. . . . . . . 8 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
175		fofi 9273	. . . . . . . 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)
176	169, 174, 175	mp2an 704	. . . . . . 7 ⊢ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin
177	155, 153	elrnmpti 5953	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧))
178		elgz 16991	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧ (ℜ‘𝑧) ∈ ℤ ∧ (ℑ‘𝑧) ∈ ℤ))
179	178	simp2bi 1162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℜ‘𝑧) ∈ ℤ)
180	179	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℤ)
181	180	zcnd 12701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℂ)
182	181	abscld 15490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ∈ ℝ)
183	4	ad2antlr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ)
184	183	abscld 15490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈ ℝ)
185		simpllr 787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ+)
186	185	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ+)
187	186	rpred 13060	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ)
188		simplrl 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ)
189	188	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ)
190	187, 189	readdcld 11238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ)
191	190, 186	rerpdivcld 13091	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ)
192	191	flcld 13831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ)
193	192	peano2zd 12703	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
194	193	zred 12700	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ)
195		absrele 15359	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
196	183, 195	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
197	186	rpcnd 13062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ)
198	197, 183	absmuld 15508	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧)))
199	186	rpge0d 13064	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟)
200	187, 199	absidd 15474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟)
201	200	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧)))
202	198, 201	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧)))
203		simplrr 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
204		sslin 4203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
205	203, 204	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
206	139	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (abs ∘ − ) ∈ (∞Met‘ℂ))
207	6	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
208	163	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 0 ∈ ℂ)
209	185	rpxrd 13061	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ*)
210	188	rexrd 11259	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ*)
211		bldisj 24524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅)
212	211	3exp2 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → (𝑟 ∈ ℝ* → (𝑑 ∈ ℝ* → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))))
213	212	imp32 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ* ∧ 𝑑 ∈ ℝ*)) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
214	206, 207, 208, 209, 210, 213	syl32anc 1403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
215		sseq0 4367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅)
216	205, 214, 215	syl6an 696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅))
217	216	necon3ad 2977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)))
218	217	imp 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))
219		rexadd 13258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
220	187, 189, 219	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑))
221	207	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ)
222	123	cnmetdval 24896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
223	221, 163, 222	sylancl 597	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
224	221	subid1d 11558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧))
225	224	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧)))
226	223, 225	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧)))
227	220, 226	breq12d 5126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) ↔ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
228	218, 227	mtbid 327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))
229	221	abscld 15490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ)
230	229, 190	ltnled 11357	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
231	228, 230	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑))
232	202, 231	eqbrtrrd 5139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑))
233	184, 190, 186	ltmuldiv2d 13108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)))
234	232, 233	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))
235		flltp1 13833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
236	191, 235	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
237	184, 191, 194, 234, 236	lttrd 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
238	184, 194, 237	ltled 11358	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
239	182, 184, 194, 196, 238	letrd 11367	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
240	180	zred 12700	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℝ)
241	240, 194	absled 15484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
242	239, 241	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
243	193	znegcld 12702	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
244		elfz 13541	. . . . . . . . . . . . . . . . 17 ⊢ (((ℜ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
245	180, 243, 193, 244	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
246	242, 245	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
247	178	simp3bi 1163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℑ‘𝑧) ∈ ℤ)
248	247	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℤ)
249	248	zcnd 12701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℂ)
250	249	abscld 15490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ∈ ℝ)
251		absimle 15360	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧))
252	183, 251	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧))
253	250, 184, 194, 252, 238	letrd 11367	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
254	248	zred 12700	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℝ)
255	254, 194	absled 15484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
256	253, 255	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
257		elfz 13541	. . . . . . . . . . . . . . . . 17 ⊢ (((ℑ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
258	248, 243, 193, 257	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
259	256, 258	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
260	183	replimd 15248	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
261	260	oveq2d 7427	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
262		oveq1 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏)))
263	262	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))
264	263	eqeq2d 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))))
265		oveq2 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i · (ℑ‘𝑧)))
266	265	oveq2d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
267	266	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
268	267	eqeq2d 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))))
269	264, 268	rspc2ev 3603	. . . . . . . . . . . . . . 15 ⊢ (((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
270	246, 259, 261, 269	syl3anc 1396	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
271	270	ex 417	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))))
272	170, 171	elrnmpo 7547	. . . . . . . . . . . . 13 ⊢ ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
273	271, 272	imbitrrdi 255	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
274	156	ineq1d 4180	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
275	274	neeq1d 3023	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅))
276		eleq1 2857	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
277	275, 276	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
278	273, 277	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
279	278	rexlimdva 3172	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
280	177, 279	biimtrid 245	. . . . . . . . 9 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
281	280	3imp 1126	. . . . . . . 8 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
282	281	rabssdv 4036	. . . . . . 7 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
283		ssfi 9157	. . . . . . 7 ⊢ ((ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
284	176, 282, 283	sylancr 598	. . . . . 6 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
285	166, 284	rexlimddv 3178	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
286		iuneq1 4977	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
287	286	sseq2d 3977	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
288		rabeq 3437	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅})
289	288	eleq1d 2854	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
290	287, 289	anbi12d 643	. . . . . 6 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
291	290	rspcev 3590	. . . . 5 ⊢ ((ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ∧ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
292	11, 162, 285, 291	syl12anc 849	. . . 4 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
293	292	ralrimiva 3163	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
294	13	sstotbnd3 38315	. . . 4 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
295	12, 15, 294	sylancr 598	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
296	293, 295	mpbird 260	. 2 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋))
297	1, 296	impbii 212	1 ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  {crab 3423  Vcvv 3463   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  𝒫 cpw 4567  ∪ ciun 4960   class class class wbr 5113   ↦ cmpt 5196   × cxp 5660  ran crn 5663   ↾ cres 5664   ∘ ccom 5666   Fn wfn 6532  –onto→wfo 6535  ‘cfv 6537  (class class class)co 7411   ∈ cmpo 7413  Fincfn 8943  ℂcc 11098  ℝcr 11099  0cc0 11100  1c1 11101  ici 11102   + caddc 11103   · cmul 11105  ℝ^*cxr 11242   < clt 11243   ≤ cle 11244   − cmin 11441  -cneg 11442   / cdiv 11871  2c2 12295  ℤcz 12591  ℝ⁺crp 13016   +_𝑒 cxad 13135  ...cfz 13535  ⌊cfl 13823  ↑cexp 14097  ℜcre 15148  ℑcim 15149  abscabs 15285  ℤ[i]cgz 16989  ∞Metcxmet 21476  Metcmet 21477  ballcbl 21478  TotBndctotbnd 38305  Bndcbnd 38306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177  ax-pre-sup 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-er 8694  df-ec 8696  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9402  df-inf 9403  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-nn 12234  df-2 12303  df-3 12304  df-n0 12505  df-z 12592  df-uz 12863  df-rp 13017  df-xneg 13137  df-xadd 13138  df-xmul 13139  df-fz 13536  df-fl 13825  df-seq 14038  df-exp 14098  df-cj 15150  df-re 15151  df-im 15152  df-sqrt 15286  df-abs 15287  df-gz 16990  df-psmet 21483  df-xmet 21484  df-met 21485  df-bl 21486  df-totbnd 38307  df-bnd 38318

This theorem is referenced by:  cnpwstotbnd  38336