cntotbnd - Mathbox for Jeff Madsen

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

Theorem cntotbnd 35640

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 35633	. 2 ⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋))
2		rpcn 12561	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℂ)
3	2	adantl 485	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℂ)
4		gzcn 16448	. . . . . . . . 9 ⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ)
5		mulcl 10778	. . . . . . . . 9 ⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ)
6	3, 4, 5	syl2an 599	. . . . . . . 8 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
7	6	fmpttd 6910	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)):ℤ[i]⟶ℂ)
8	7	frnd 6531	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
9		cnex 10775	. . . . . . 7 ⊢ ℂ ∈ V
10	9	elpw2 5223	. . . . . 6 ⊢ (ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ↔ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ⊆ ℂ)
11	8, 10	sylibr 237	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ)
12		cnmet 23623	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (Met‘ℂ)
13		cntotbnd.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))
14	13	bnd2lem 35635	. . . . . . . . . . . . . . . . 17 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ)
15	12, 14	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ)
16	15	sselda 3887	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ)
17	16	adantrl 716	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ)
18	17	recld 14722	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ)
19		simprl 771	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ⁺)
20	18, 19	rerpdivcld 12624	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ)
21		halfre 12009	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
22		readdcl 10777	. . . . . . . . . . . 12 ⊢ ((((ℜ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
23	20, 21, 22	sylancl 589	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
24	23	flcld 13338	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
25	17	imcld 14723	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ)
26	25, 19	rerpdivcld 12624	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ)
27		readdcl 10777	. . . . . . . . . . . 12 ⊢ ((((ℑ‘𝑦) / 𝑟) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
28	26, 21, 27	sylancl 589	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ)
29	28	flcld 13338	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ)
30		gzreim 16455	. . . . . . . . . 10 ⊢ (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
31	24, 29, 30	syl2anc 587	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i])
32		gzcn 16448	. . . . . . . . . . . . . . 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 12595	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ)
35	19	rpne0d 12598	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0)
36	17, 34, 35	divcld 11573	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ)
37	33, 36	subcld 11154	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ)
38	37	abscld 14965	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ)
39		1re 10798	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ)
41	24	zcnd 12248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
42		ax-icn 10753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ i ∈ ℂ
43	29	zcnd 12248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ)
44		mulcl 10778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
45	42, 43, 44	sylancr 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈ ℂ)
46	20	recnd 10826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ)
47	26	recnd 10826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ)
48		mulcl 10778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
49	42, 47, 48	sylancr 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
50	41, 45, 46, 49	addsub4d 11201	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
51	36	replimd 14725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))))
52	19	rpred 12593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ)
53	52, 17, 35	redivd 14757	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟))
54	52, 17, 35	imdivd 14758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟))
55	54	oveq2d 7207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟)))
56	53, 55	oveq12d 7209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
57	51, 56	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))
58	57	oveq2d 7207	. . . . . . . . . . . . . . . . . . 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 11253	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟))))
61	60	oveq2d 7207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i · ((ℑ‘𝑦) / 𝑟)))))
62	50, 58, 61	3eqtr4d 2781	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))
63	62	fveq2d 6699	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))))
64	63	oveq1d 7206	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2))
65	24	zred 12247	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
66	65, 20	resubcld 11225	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ)
67	29	zred 12247	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℝ)
68	67, 26	resubcld 11225	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ)
69		absreimsq 14821	. . . . . . . . . . . . . . . . 17 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧ ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
70	66, 68, 69	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i · ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
71	64, 70	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) = ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)))
72	66	resqcld 13782	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ)
73	68	resqcld 13782	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ)
74	21	resqcli 13720	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) ∈ ℝ
75	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈ ℝ)
76	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈ ℝ)
77		absresq 14831	. . . . . . . . . . . . . . . . . . 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 14869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℜ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
80	20, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2))
81	66	recnd 10826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ)
82	81	abscld 14965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ)
83	81	absge0d 14973	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))))
84		halfgt0 12011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < (1 / 2)
85	21, 84	elrpii 12554	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) ∈ ℝ⁺
86		rpge0 12564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 / 2) ∈ ℝ⁺ → 0 ≤ (1 / 2))
87	85, 86	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2))
88	82, 76, 83, 87	le2sqd 13791	. . . . . . . . . . . . . . . . . . 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 5063	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
91		halfcn 12010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 2) ∈ ℂ
92	91	sqvali 13714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2)↑2) = ((1 / 2) · (1 / 2))
93		halflt1 12013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) < 1
94	21, 39, 21, 84	ltmul1ii 11725	. . . . . . . . . . . . . . . . . . . . 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	mulid2i 10803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 · (1 / 2)) = (1 / 2)
97	95, 96	breqtri 5064	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) · (1 / 2)) < (1 / 2)
98	92, 97	eqbrtri 5060	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2)↑2) < (1 / 2)
99	98	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 / 2))
100	72, 75, 76, 90, 99	lelttrd 10955	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2))
101		absresq 14831	. . . . . . . . . . . . . . . . . . 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 14869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℑ‘𝑦) / 𝑟) ∈ ℝ → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
104	26, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2))
105	68	recnd 10826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ)
106	105	abscld 14965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ)
107	105	absge0d 14973	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))
108	106, 76, 107, 87	le2sqd 13791	. . . . . . . . . . . . . . . . . . 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 5063	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 / 2)↑2))
111	73, 75, 76, 110, 99	lelttrd 10955	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2))
112	72, 73, 40, 100, 111	lt2halvesd 12043	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) + (((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1)
113	71, 112	eqbrtrd 5061	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1)
114		sq1 13729	. . . . . . . . . . . . . 14 ⊢ (1↑2) = 1
115	113, 114	breqtrrdi 5081	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2))
116	37	absge0d 14973	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))
117		0le1 11320	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
118	117	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1)
119	38, 40, 116, 118	lt2sqd 13790	. . . . . . . . . . . . 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 12649	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1))
122	34, 33	mulcld 10818	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ)
123		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) = (abs ∘ − )
124	123	cnmetdval 23622	. . . . . . . . . . . . 13 ⊢ (((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
125	122, 17, 124	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
126	34, 33, 36	subdid 11253	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))))
127	17, 34, 35	divcan2d 11575	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦)
128	127	oveq2d 7207	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
129	126, 128	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))
130	129	fveq2d 6699	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)))
131	34, 37	absmuld 14983	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 · (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
132	130, 131	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
133	19	rpge0d 12597	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟)
134	52, 133	absidd 14951	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟)
135	134	oveq1d 7206	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))))
136	125, 132, 135	3eqtrrd 2776	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦))
137	34	mulid1d 10815	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟)
138	121, 136, 137	3brtr3d 5070	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)
139		cnxmet 23624	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
140	139	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
141		rpxr 12560	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
142	141	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ^*)
143		elbl2 23242	. . . . . . . . . . 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 839	. . . . . . . . . 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 7199	. . . . . . . . . . . 12 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))))
147	146	oveq1d 7206	. . . . . . . . . . 11 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟))
148	147	eleq2d 2816	. . . . . . . . . 10 ⊢ (𝑧 = ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)))
149	148	rspcev 3527	. . . . . . . . 9 ⊢ ((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 · ((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i · (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
150	31, 145, 149	syl2anc 587	. . . . . . . 8 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
151	150	expr 460	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
152		eliun 4894	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
153		ovex 7224	. . . . . . . . . 10 ⊢ (𝑟 · 𝑧) ∈ V
154	153	rgenw 3063	. . . . . . . . 9 ⊢ ∀𝑧 ∈ ℤ[i] (𝑟 · 𝑧) ∈ V
155		eqid 2736	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))
156		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))
157	156	eleq2d 2816	. . . . . . . . . 10 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)))
158	155, 157	rexrnmptw 6892	. . . . . . . . 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	syl6ibr 255	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
162	161	ssrdv 3893	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
163		simpl 486	. . . . . . 7 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝐷 ∈ (Bnd‘𝑋))
164		0cn 10790	. . . . . . . 8 ⊢ 0 ∈ ℂ
165	13	ssbnd 35632	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) → (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑)))
166	12, 164, 165	mp2an 692	. . . . . . 7 ⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
167	163, 166	sylib 221	. . . . . 6 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
168		fzfi 13510	. . . . . . . . 9 ⊢ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin
169		xpfi 8920	. . . . . . . . 9 ⊢ (((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) → ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin)
170	168, 168, 169	mp2an 692	. . . . . . . 8 ⊢ ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin
171		eqid 2736	. . . . . . . . . 10 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
172		ovex 7224	. . . . . . . . . 10 ⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V
173	171, 172	fnmpoi 7818	. . . . . . . . 9 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
174		dffn4 6617	. . . . . . . . 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 233	. . . . . . . 8 ⊢ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))
176		fofi 8940	. . . . . . . 8 ⊢ ((((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin ∧ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin)
177	170, 175, 176	mp2an 692	. . . . . . 7 ⊢ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin
178	155, 153	elrnmpti 5814	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧))
179		elgz 16447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧ (ℜ‘𝑧) ∈ ℤ ∧ (ℑ‘𝑧) ∈ ℤ))
180	179	simp2bi 1148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℜ‘𝑧) ∈ ℤ)
181	180	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℤ)
182	181	zcnd 12248	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℂ)
183	182	abscld 14965	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ∈ ℝ)
184	4	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ)
185	184	abscld 14965	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈ ℝ)
186		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ⁺)
187	186	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ⁺)
188	187	rpred 12593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ)
189		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ)
190	189	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ)
191	188, 190	readdcld 10827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ)
192	191, 187	rerpdivcld 12624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ)
193	192	flcld 13338	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ)
194	193	peano2zd 12250	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
195	194	zred 12247	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ)
196		absrele 14837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℂ → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
197	184, 196	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧))
198	187	rpcnd 12595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ)
199	198, 184	absmuld 14983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧)))
200	187	rpge0d 12597	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟)
201	188, 200	absidd 14951	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟)
202	201	oveq1d 7206	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧)))
203	199, 202	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧)))
204		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))
205		sslin 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)))
207	139	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (abs ∘ − ) ∈ (∞Met‘ℂ))
208	6	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑟 · 𝑧) ∈ ℂ)
209	164	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 0 ∈ ℂ)
210	186	rpxrd 12594	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑟 ∈ ℝ^*)
211	189	rexrd 10848	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → 𝑑 ∈ ℝ^*)
212		bldisj 23250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ^* ∧ 𝑑 ∈ ℝ^* ∧ (𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅)
213	212	3exp2 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → (𝑟 ∈ ℝ^* → (𝑑 ∈ ℝ^* → ((𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))))
214	213	imp32 422	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) ∧ (𝑟 ∈ ℝ^* ∧ 𝑑 ∈ ℝ^*)) → ((𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
215	207, 208, 209, 210, 211, 214	syl32anc 1380	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅))
216		sseq0 4300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅)
217	206, 215, 216	syl6an 684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅))
218	217	necon3ad 2945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ¬ (𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)))
219	218	imp 410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))
220		rexadd 12787	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +_𝑒 𝑑) = (𝑟 + 𝑑))
221	188, 190, 220	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +_𝑒 𝑑) = (𝑟 + 𝑑))
222	208	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ)
223	123	cnmetdval 23622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
224	222, 164, 223	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘((𝑟 · 𝑧) − 0)))
225	222	subid1d 11143	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧))
226	225	fveq2d 6699	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧)))
227	224, 226	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧)))
228	221, 227	breq12d 5052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 +_𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) ↔ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
229	219, 228	mtbid 327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))
230	222	abscld 14965	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ)
231	230, 191	ltnled 10944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))))
232	229, 231	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑))
233	203, 232	eqbrtrrd 5063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑))
234	185, 191, 187	ltmuldiv2d 12641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)))
235	233, 234	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))
236		flltp1 13340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
237	192, 236	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
238	185, 192, 195, 235, 237	lttrd 10958	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
239	185, 195, 238	ltled 10945	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
240	183, 185, 195, 197, 239	letrd 10954	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
241	181	zred 12247	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ ℝ)
242	241, 195	absled 14959	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
243	240, 242	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
244	194	znegcld 12249	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ)
245		elfz 13066	. . . . . . . . . . . . . . . . 17 ⊢ (((ℜ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
246	181, 244, 194, 245	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
247	243, 246	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
248	179	simp3bi 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℤ[i] → (ℑ‘𝑧) ∈ ℤ)
249	248	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℤ)
250	249	zcnd 12248	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℂ)
251	250	abscld 14965	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ∈ ℝ)
252		absimle 14838	. . . . . . . . . . . . . . . . . . 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 10954	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))
255	249	zred 12247	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ ℝ)
256	255, 195	absled 14959	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
257	254, 256	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
258		elfz 13066	. . . . . . . . . . . . . . . . 17 ⊢ (((ℑ‘𝑧) ∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
259	249, 244, 194, 258	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))))
260	257, 259	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))
261	184	replimd 14725	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
262	261	oveq2d 7207	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
263		oveq1 7198	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏)))
264	263	oveq2d 7207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))
265	264	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))))
266		oveq2 7199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i · (ℑ‘𝑧)))
267	266	oveq2d 7207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
268	267	oveq2d 7207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))
269	268	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))))
270	265, 269	rspc2ev 3539	. . . . . . . . . . . . . . 15 ⊢ (((ℜ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
271	247, 260, 262, 270	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
272	271	ex 416	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))))
273	171, 172	elrnmpo 7324	. . . . . . . . . . . . 13 ⊢ ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))
274	272, 273	syl6ibr 255	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
275	156	ineq1d 4112	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
276	275	neeq1d 2991	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅))
277		eleq1 2818	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))
278	276, 277	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
279	274, 278	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) → (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
280	279	rexlimdva 3193	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
281	178, 280	syl5bi 245	. . . . . . . . 9 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))))
282	281	3imp 1113	. . . . . . . 8 ⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
283	282	rabssdv 3974	. . . . . . 7 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))
284		ssfi 8829	. . . . . . 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 590	. . . . . 6 ⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs ∘ − ))𝑑))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
286	167, 285	rexlimddv 3200	. . . . 5 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)
287		iuneq1 4906	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))
288	287	sseq2d 3919	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)))
289		rabeq 3384	. . . . . . . 8 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅})
290	289	eleq1d 2815	. . . . . . 7 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
291	288, 290	anbi12d 634	. . . . . 6 ⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
292	291	rspcev 3527	. . . . 5 ⊢ ((ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ ∧ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
293	11, 162, 286, 292	syl12anc 837	. . . 4 ⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
294	293	ralrimiva 3095	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ⁺ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin))
295	13	sstotbnd3 35620	. . . 4 ⊢ (((abs ∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ⁺ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
296	12, 15, 295	sylancr 590	. . 3 ⊢ (𝐷 ∈ (Bnd‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ⁺ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)))
297	294, 296	mpbird 260	. 2 ⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋))
298	1, 297	impbii 212	1 ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2112 ≠ wne 2932 ∀wral 3051 ∃wrex 3052 {crab 3055 Vcvv 3398 ∩ cin 3852 ⊆ wss 3853 ∅c0 4223 𝒫 cpw 4499 ∪ ciun 4890 class class class wbr 5039 ↦ cmpt 5120 × cxp 5534 ran crn 5537 ↾ cres 5538 ∘ ccom 5540 Fn wfn 6353 –onto→wfo 6356 ‘cfv 6358 (class class class)co 7191 ∈ cmpo 7193 Fincfn 8604 ℂcc 10692 ℝcr 10693 0cc0 10694 1c1 10695 ici 10696 + caddc 10697 · cmul 10699 ℝ^*cxr 10831 < clt 10832 ≤ cle 10833 − cmin 11027 -cneg 11028 / cdiv 11454 2c2 11850 ℤcz 12141 ℝ⁺crp 12551 +_𝑒 cxad 12667 ...cfz 13060 ⌊cfl 13330 ↑cexp 13600 ℜcre 14625 ℑcim 14626 abscabs 14762 ℤ[i]cgz 16445 ∞Metcxmet 20302 Metcmet 20303 ballcbl 20304 TotBndctotbnd 35610 Bndcbnd 35611

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 ax-cnex 10750 ax-resscn 10751 ax-1cn 10752 ax-icn 10753 ax-addcl 10754 ax-addrcl 10755 ax-mulcl 10756 ax-mulrcl 10757 ax-mulcom 10758 ax-addass 10759 ax-mulass 10760 ax-distr 10761 ax-i2m1 10762 ax-1ne0 10763 ax-1rid 10764 ax-rnegex 10765 ax-rrecex 10766 ax-cnre 10767 ax-pre-lttri 10768 ax-pre-lttrn 10769 ax-pre-ltadd 10770 ax-pre-mulgt0 10771 ax-pre-sup 10772

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6140 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7148 df-ov 7194 df-oprab 7195 df-mpo 7196 df-om 7623 df-1st 7739 df-2nd 7740 df-wrecs 8025 df-recs 8086 df-rdg 8124 df-1o 8180 df-er 8369 df-ec 8371 df-map 8488 df-en 8605 df-dom 8606 df-sdom 8607 df-fin 8608 df-sup 9036 df-inf 9037 df-pnf 10834 df-mnf 10835 df-xr 10836 df-ltxr 10837 df-le 10838 df-sub 11029 df-neg 11030 df-div 11455 df-nn 11796 df-2 11858 df-3 11859 df-n0 12056 df-z 12142 df-uz 12404 df-rp 12552 df-xneg 12669 df-xadd 12670 df-xmul 12671 df-fz 13061 df-fl 13332 df-seq 13540 df-exp 13601 df-cj 14627 df-re 14628 df-im 14629 df-sqrt 14763 df-abs 14764 df-gz 16446 df-psmet 20309 df-xmet 20310 df-met 20311 df-bl 20312 df-totbnd 35612 df-bnd 35623

This theorem is referenced by: cnpwstotbnd 35641

W3C validator