cntotbnd

Description: A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015)

		Ref	Expression
	Hypothesis	cntotbnd.d	$⊢ D = {(abs \circ -) ↾}_{(X \times X)}$
	Assertion	cntotbnd	$⊢ D \in TotBnd (X) \leftrightarrow D \in Bnd (X)$

Proof

Step	Hyp	Ref	Expression
1		cntotbnd.d	$⊢ D = {(abs \circ -) ↾}_{(X \times X)}$
2		totbndbnd	$⊢ D \in TotBnd (X) \to D \in Bnd (X)$
3		rpcn	$⊢ r \in ℝ^{+} \to r \in ℂ$
4	3	adantl	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to r \in ℂ$
5		gzcn	$⊢ z \in ℤ [i] \to z \in ℂ$
6		mulcl	$⊢ (r \in ℂ \land z \in ℂ) \to r z \in ℂ$
7	4 5 6	syl2an	$⊢ ((D \in Bnd (X) \land r \in ℝ^{+}) \land z \in ℤ [i]) \to r z \in ℂ$
8	7	fmpttd	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to (z \in ℤ [i] ⟼ r z) : ℤ [i] ⟶ ℂ$
9	8	frnd	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to ran (z \in ℤ [i] ⟼ r z) \subseteq ℂ$
10		cnex	$⊢ ℂ \in V$
11	10	elpw2	$⊢ ran (z \in ℤ [i] ⟼ r z) \in 𝒫 ℂ \leftrightarrow ran (z \in ℤ [i] ⟼ r z) \subseteq ℂ$
12	9 11	sylibr	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to ran (z \in ℤ [i] ⟼ r z) \in 𝒫 ℂ$
13		cnmet	$⊢ abs \circ - \in Met (ℂ)$
14	1	bnd2lem	$⊢ (abs \circ - \in Met (ℂ) \land D \in Bnd (X)) \to X \subseteq ℂ$
15	13 14	mpan	$⊢ D \in Bnd (X) \to X \subseteq ℂ$
16	15	sselda	$⊢ (D \in Bnd (X) \land y \in X) \to y \in ℂ$
17	16	adantrl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to y \in ℂ$
18	17	recld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ℜ (y) \in ℝ$
19		simprl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \in ℝ^{+}$
20	18 19	rerpdivcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{ℜ (y)}{r} \in ℝ$
21		halfre	$⊢ \frac{1}{2} \in ℝ$
22		readdcl	$⊢ (\frac{ℜ (y)}{r} \in ℝ \land \frac{1}{2} \in ℝ) \to (\frac{ℜ (y)}{r}) + (\frac{1}{2}) \in ℝ$
23	20 21 22	sylancl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to (\frac{ℜ (y)}{r}) + (\frac{1}{2}) \in ℝ$
24	23	flcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ$
25	17	imcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ℑ (y) \in ℝ$
26	25 19	rerpdivcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{ℑ (y)}{r} \in ℝ$
27		readdcl	$⊢ (\frac{ℑ (y)}{r} \in ℝ \land \frac{1}{2} \in ℝ) \to (\frac{ℑ (y)}{r}) + (\frac{1}{2}) \in ℝ$
28	26 21 27	sylancl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to (\frac{ℑ (y)}{r}) + (\frac{1}{2}) \in ℝ$
29	28	flcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ$
30		gzreim	$⊢ (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ \land ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ [i]$
31	24 29 30	syl2anc	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ [i]$
32		gzcn	$⊢ ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ [i] \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ$
33	31 32	syl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ$
34	19	rpcnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \in ℂ$
35	19	rpne0d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \neq 0$
36	17 34 35	divcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{y}{r} \in ℂ$
37	33 36	subcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r}) \in ℂ$
38	37	abscld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| \in ℝ$
39		1re	$⊢ 1 \in ℝ$
40	39	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 1 \in ℝ$
41	24	zcnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ$
42		ax-icn	$⊢ i \in ℂ$
43	29	zcnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ$
44		mulcl	$⊢ (i \in ℂ \land ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ) \to i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ$
45	42 43 44	sylancr	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℂ$
46	20	recnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{ℜ (y)}{r} \in ℂ$
47	26	recnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{ℑ (y)}{r} \in ℂ$
48		mulcl	$⊢ (i \in ℂ \land \frac{ℑ (y)}{r} \in ℂ) \to i (\frac{ℑ (y)}{r}) \in ℂ$
49	42 47 48	sylancr	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to i (\frac{ℑ (y)}{r}) \in ℂ$
50	41 45 46 49	addsub4d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - ((\frac{ℜ (y)}{r}) + i (\frac{ℑ (y)}{r})) = (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})) + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - i (\frac{ℑ (y)}{r})$
51	36	replimd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{y}{r} = ℜ (\frac{y}{r}) + i ℑ (\frac{y}{r})$
52	19	rpred	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \in ℝ$
53	52 17 35	redivd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ℜ (\frac{y}{r}) = \frac{ℜ (y)}{r}$
54	52 17 35	imdivd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ℑ (\frac{y}{r}) = \frac{ℑ (y)}{r}$
55	54	oveq2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to i ℑ (\frac{y}{r}) = i (\frac{ℑ (y)}{r})$
56	53 55	oveq12d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ℜ (\frac{y}{r}) + i ℑ (\frac{y}{r}) = (\frac{ℜ (y)}{r}) + i (\frac{ℑ (y)}{r})$
57	51 56	eqtrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{y}{r} = (\frac{ℜ (y)}{r}) + i (\frac{ℑ (y)}{r})$
58	57	oveq2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r}) = ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - ((\frac{ℜ (y)}{r}) + i (\frac{ℑ (y)}{r}))$
59	42	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to i \in ℂ$
60	59 43 47	subdid	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})) = i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - i (\frac{ℑ (y)}{r})$
61	60	oveq2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) + i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})) = (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})) + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - i (\frac{ℑ (y)}{r})$
62	50 58 61	3eqtr4d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r}) = ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) + i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))$
63	62	fveq2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| = \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) + i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))\|$
64	63	oveq1d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|}^{2} = {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) + i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))\|}^{2}$
65	24	zred	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ \in ℝ$
66	65 20	resubcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) \in ℝ$
67	29	zred	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℝ$
68	67 26	resubcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}) \in ℝ$
69		absreimsq	$⊢ (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) \in ℝ \land ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}) \in ℝ) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) + i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))\|}^{2} = {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} + {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2}$
70	66 68 69	syl2anc	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) + i (⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))\|}^{2} = {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} + {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2}$
71	64 70	eqtrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|}^{2} = {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} + {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2}$
72	66	resqcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} \in ℝ$
73	68	resqcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2} \in ℝ$
74	21	resqcli	$⊢ {(\frac{1}{2})}^{2} \in ℝ$
75	74	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(\frac{1}{2})}^{2} \in ℝ$
76	21	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \frac{1}{2} \in ℝ$
77		absresq	$⊢ ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) \in ℝ \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\|}^{2} = {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2}$
78	66 77	syl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\|}^{2} = {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2}$
79		rddif	$⊢ \frac{ℜ (y)}{r} \in ℝ \to \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\| \leq \frac{1}{2}$
80	20 79	syl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\| \leq \frac{1}{2}$
81	66	recnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}) \in ℂ$
82	81	abscld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\| \in ℝ$
83	81	absge0d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 0 \leq \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\|$
84		halfgt0	$⊢ 0 < \frac{1}{2}$
85	21 84	elrpii	$⊢ \frac{1}{2} \in ℝ^{+}$
86		rpge0	$⊢ \frac{1}{2} \in ℝ^{+} \to 0 \leq \frac{1}{2}$
87	85 86	mp1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 0 \leq \frac{1}{2}$
88	82 76 83 87	le2sqd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to (\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\| \leq \frac{1}{2} \leftrightarrow {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\|}^{2} \leq {(\frac{1}{2})}^{2})$
89	80 88	mpbid	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r})\|}^{2} \leq {(\frac{1}{2})}^{2}$
90	78 89	eqbrtrrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} \leq {(\frac{1}{2})}^{2}$
91		halfcn	$⊢ \frac{1}{2} \in ℂ$
92	91	sqvali	$⊢ {(\frac{1}{2})}^{2} = (\frac{1}{2}) (\frac{1}{2})$
93		halflt1	$⊢ \frac{1}{2} < 1$
94	21 39 21 84	ltmul1ii	$⊢ \frac{1}{2} < 1 \leftrightarrow (\frac{1}{2}) (\frac{1}{2}) < 1 (\frac{1}{2})$
95	93 94	mpbi	$⊢ (\frac{1}{2}) (\frac{1}{2}) < 1 (\frac{1}{2})$
96	91	mullidi	$⊢ 1 (\frac{1}{2}) = \frac{1}{2}$
97	95 96	breqtri	$⊢ (\frac{1}{2}) (\frac{1}{2}) < \frac{1}{2}$
98	92 97	eqbrtri	$⊢ {(\frac{1}{2})}^{2} < \frac{1}{2}$
99	98	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(\frac{1}{2})}^{2} < \frac{1}{2}$
100	72 75 76 90 99	lelttrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} < \frac{1}{2}$
101		absresq	$⊢ ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}) \in ℝ \to {\|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\|}^{2} = {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2}$
102	68 101	syl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\|}^{2} = {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2}$
103		rddif	$⊢ \frac{ℑ (y)}{r} \in ℝ \to \|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\| \leq \frac{1}{2}$
104	26 103	syl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\| \leq \frac{1}{2}$
105	68	recnd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}) \in ℂ$
106	105	abscld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\| \in ℝ$
107	105	absge0d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 0 \leq \|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\|$
108	106 76 107 87	le2sqd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to (\|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\| \leq \frac{1}{2} \leftrightarrow {\|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\|}^{2} \leq {(\frac{1}{2})}^{2})$
109	104 108	mpbid	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r})\|}^{2} \leq {(\frac{1}{2})}^{2}$
110	102 109	eqbrtrrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2} \leq {(\frac{1}{2})}^{2}$
111	73 75 76 110 99	lelttrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2} < \frac{1}{2}$
112	72 73 40 100 111	lt2halvesd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {(⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℜ (y)}{r}))}^{2} + {(⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{ℑ (y)}{r}))}^{2} < 1$
113	71 112	eqbrtrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|}^{2} < 1$
114		sq1	$⊢ 1^{2} = 1$
115	113 114	breqtrrdi	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|}^{2} < 1^{2}$
116	37	absge0d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 0 \leq \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|$
117		0le1	$⊢ 0 \leq 1$
118	117	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 0 \leq 1$
119	38 40 116 118	lt2sqd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to (\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| < 1 \leftrightarrow {\|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|}^{2} < 1^{2})$
120	115 119	mpbird	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| < 1$
121	38 40 19 120	ltmul2dd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| < r \cdot 1$
122	34 33	mulcld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) \in ℂ$
123		eqid	$⊢ abs \circ - = abs \circ -$
124	123	cnmetdval	$⊢ (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) \in ℂ \land y \in ℂ) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) (abs \circ -) y = \|r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - y\|$
125	122 17 124	syl2anc	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) (abs \circ -) y = \|r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - y\|$
126	34 33 36	subdid	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})) = r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - r (\frac{y}{r})$
127	17 34 35	divcan2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (\frac{y}{r}) = y$
128	127	oveq2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - r (\frac{y}{r}) = r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - y$
129	126 128	eqtrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})) = r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - y$
130	129	fveq2d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r}))\| = \|r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - y\|$
131	34 37	absmuld	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r}))\| = \|r\| \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|$
132	130 131	eqtr3d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) - y\| = \|r\| \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|$
133	19	rpge0d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to 0 \leq r$
134	52 133	absidd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|r\| = r$
135	134	oveq1d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \|r\| \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| = r \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\|$
136	125 132 135	3eqtrrd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \|⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ - (\frac{y}{r})\| = r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) (abs \circ -) y$
137	34	mulridd	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \cdot 1 = r$
138	121 136 137	3brtr3d	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) (abs \circ -) y < r$
139		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
140	139	a1i	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to abs \circ - \in ∞Met (ℂ)$
141		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
142	141	ad2antrl	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to r \in ℝ^{*}$
143		elbl2	$⊢ ((abs \circ - \in ∞Met (ℂ) \land r \in ℝ^{*}) \land (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) \in ℂ \land y \in ℂ)) \to (y \in (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) ball (abs \circ -) r) \leftrightarrow r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) (abs \circ -) y < r)$
144	140 142 122 17 143	syl22anc	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to (y \in (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) ball (abs \circ -) r) \leftrightarrow r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) (abs \circ -) y < r)$
145	138 144	mpbird	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to y \in (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) ball (abs \circ -) r)$
146		oveq2	$⊢ z = ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \to r z = r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋)$
147	146	oveq1d	$⊢ z = ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \to r z ball (abs \circ -) r = r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) ball (abs \circ -) r$
148	147	eleq2d	$⊢ z = ⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \to (y \in (r z ball (abs \circ -) r) \leftrightarrow y \in (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) ball (abs \circ -) r))$
149	148	rspcev	$⊢ (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋ \in ℤ [i] \land y \in (r (⌊(\frac{ℜ (y)}{r}) + (\frac{1}{2})⌋ + i ⌊(\frac{ℑ (y)}{r}) + (\frac{1}{2})⌋) ball (abs \circ -) r)) \to \exists z \in ℤ [i] y \in (r z ball (abs \circ -) r)$
150	31 145 149	syl2anc	$⊢ (D \in Bnd (X) \land (r \in ℝ^{+} \land y \in X)) \to \exists z \in ℤ [i] y \in (r z ball (abs \circ -) r)$
151	150	expr	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to (y \in X \to \exists z \in ℤ [i] y \in (r z ball (abs \circ -) r))$
152		eliun	$⊢ y \in ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r) \leftrightarrow \exists x \in ran (z \in ℤ [i] ⟼ r z) y \in (x ball (abs \circ -) r)$
153		ovex	$⊢ r z \in V$
154	153	rgenw	$⊢ \forall z \in ℤ [i] r z \in V$
155		eqid	$⊢ (z \in ℤ [i] ⟼ r z) = (z \in ℤ [i] ⟼ r z)$
156		oveq1	$⊢ x = r z \to x ball (abs \circ -) r = r z ball (abs \circ -) r$
157	156	eleq2d	$⊢ x = r z \to (y \in (x ball (abs \circ -) r) \leftrightarrow y \in (r z ball (abs \circ -) r))$
158	155 157	rexrnmptw	$⊢ \forall z \in ℤ [i] r z \in V \to (\exists x \in ran (z \in ℤ [i] ⟼ r z) y \in (x ball (abs \circ -) r) \leftrightarrow \exists z \in ℤ [i] y \in (r z ball (abs \circ -) r))$
159	154 158	ax-mp	$⊢ \exists x \in ran (z \in ℤ [i] ⟼ r z) y \in (x ball (abs \circ -) r) \leftrightarrow \exists z \in ℤ [i] y \in (r z ball (abs \circ -) r)$
160	152 159	bitri	$⊢ y \in ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r) \leftrightarrow \exists z \in ℤ [i] y \in (r z ball (abs \circ -) r)$
161	151 160	imbitrrdi	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to (y \in X \to y \in ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r))$
162	161	ssrdv	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to X \subseteq ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r)$
163		0cn	$⊢ 0 \in ℂ$
164	1	ssbnd	$⊢ (abs \circ - \in Met (ℂ) \land 0 \in ℂ) \to (D \in Bnd (X) \leftrightarrow \exists d \in ℝ X \subseteq 0 ball (abs \circ -) d)$
165	13 163 164	mp2an	$⊢ D \in Bnd (X) \leftrightarrow \exists d \in ℝ X \subseteq 0 ball (abs \circ -) d$
166	165	birani	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to \exists d \in ℝ X \subseteq 0 ball (abs \circ -) d$
167		fzfi	$⊢ (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin$
168		xpfi	$⊢ ((- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin \land (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin) \to (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin$
169	167 167 168	mp2an	$⊢ (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin$
170		eqid	$⊢ (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) = (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))$
171		ovex	$⊢ r (a + i b) \in V$
172	170 171	fnmpoi	$⊢ (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) Fn ((- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1))$
173		dffn4	$⊢ (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) Fn ((- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1)) \leftrightarrow (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) : (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \underset{onto}{⟶} ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))$
174	172 173	mpbi	$⊢ (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) : (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \underset{onto}{⟶} ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))$
175		fofi	$⊢ ((- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin \land (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) : (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \times (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \underset{onto}{⟶} ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))) \to ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) \in Fin$
176	169 174 175	mp2an	$⊢ ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) \in Fin$
177	155 153	elrnmpti	$⊢ x \in ran (z \in ℤ [i] ⟼ r z) \leftrightarrow \exists z \in ℤ [i] x = r z$
178		elgz	$⊢ z \in ℤ [i] \leftrightarrow (z \in ℂ \land ℜ (z) \in ℤ \land ℑ (z) \in ℤ)$
179	178	simp2bi	$⊢ z \in ℤ [i] \to ℜ (z) \in ℤ$
180	179	ad2antlr	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℜ (z) \in ℤ$
181	180	zcnd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℜ (z) \in ℂ$
182	181	abscld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|ℜ (z)\| \in ℝ$
183	5	ad2antlr	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to z \in ℂ$
184	183	abscld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|z\| \in ℝ$
185		simpllr	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to r \in ℝ^{+}$
186	185	adantr	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r \in ℝ^{+}$
187	186	rpred	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r \in ℝ$
188		simplrl	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to d \in ℝ$
189	188	adantr	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to d \in ℝ$
190	187 189	readdcld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r + d \in ℝ$
191	190 186	rerpdivcld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \frac{r + d}{r} \in ℝ$
192	191	flcld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ⌊\frac{r + d}{r}⌋ \in ℤ$
193	192	peano2zd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ⌊\frac{r + d}{r}⌋ + 1 \in ℤ$
194	193	zred	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ⌊\frac{r + d}{r}⌋ + 1 \in ℝ$
195		absrele	$⊢ z \in ℂ \to \|ℜ (z)\| \leq \|z\|$
196	183 195	syl	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|ℜ (z)\| \leq \|z\|$
197	186	rpcnd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r \in ℂ$
198	197 183	absmuld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r z\| = \|r\| \|z\|$
199	186	rpge0d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to 0 \leq r$
200	187 199	absidd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r\| = r$
201	200	oveq1d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r\| \|z\| = r \|z\|$
202	198 201	eqtrd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r z\| = r \|z\|$
203		simplrr	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to X \subseteq 0 ball (abs \circ -) d$
204		sslin	$⊢ X \subseteq 0 ball (abs \circ -) d \to (r z ball (abs \circ -) r) \cap X \subseteq (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d)$
205	203 204	syl	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to (r z ball (abs \circ -) r) \cap X \subseteq (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d)$
206	139	a1i	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to abs \circ - \in ∞Met (ℂ)$
207	7	adantlr	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to r z \in ℂ$
208	163	a1i	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to 0 \in ℂ$
209	185	rpxrd	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to r \in ℝ^{*}$
210	188	rexrd	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to d \in ℝ^{*}$
211		bldisj	$⊢ ((abs \circ - \in ∞Met (ℂ) \land r z \in ℂ \land 0 \in ℂ) \land (r \in ℝ^{} \land d \in ℝ^{} \land r +_{𝑒} d \leq r z (abs \circ -) 0)) \to (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d) = \emptyset$
212	211	3exp2	$⊢ (abs \circ - \in ∞Met (ℂ) \land r z \in ℂ \land 0 \in ℂ) \to (r \in ℝ^{} \to (d \in ℝ^{} \to (r +_{𝑒} d \leq r z (abs \circ -) 0 \to (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d) = \emptyset)))$
213	212	imp32	$⊢ ((abs \circ - \in ∞Met (ℂ) \land r z \in ℂ \land 0 \in ℂ) \land (r \in ℝ^{} \land d \in ℝ^{})) \to (r +_{𝑒} d \leq r z (abs \circ -) 0 \to (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d) = \emptyset)$
214	206 207 208 209 210 213	syl32anc	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to (r +_{𝑒} d \leq r z (abs \circ -) 0 \to (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d) = \emptyset)$
215		sseq0	$⊢ ((r z ball (abs \circ -) r) \cap X \subseteq (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d) \land (r z ball (abs \circ -) r) \cap (0 ball (abs \circ -) d) = \emptyset) \to (r z ball (abs \circ -) r) \cap X = \emptyset$
216	205 214 215	syl6an	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to (r +_{𝑒} d \leq r z (abs \circ -) 0 \to (r z ball (abs \circ -) r) \cap X = \emptyset)$
217	216	necon3ad	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to ((r z ball (abs \circ -) r) \cap X \neq \emptyset \to \neg r +_{𝑒} d \leq r z (abs \circ -) 0)$
218	217	imp	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \neg r +_{𝑒} d \leq r z (abs \circ -) 0$
219		rexadd	$⊢ (r \in ℝ \land d \in ℝ) \to r +_{𝑒} d = r + d$
220	187 189 219	syl2anc	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r +_{𝑒} d = r + d$
221	207	adantr	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r z \in ℂ$
222	123	cnmetdval	$⊢ (r z \in ℂ \land 0 \in ℂ) \to r z (abs \circ -) 0 = \|r z - 0\|$
223	221 163 222	sylancl	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r z (abs \circ -) 0 = \|r z - 0\|$
224	221	subid1d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r z - 0 = r z$
225	224	fveq2d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r z - 0\| = \|r z\|$
226	223 225	eqtrd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r z (abs \circ -) 0 = \|r z\|$
227	220 226	breq12d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (r +_{𝑒} d \leq r z (abs \circ -) 0 \leftrightarrow r + d \leq \|r z\|)$
228	218 227	mtbid	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \neg r + d \leq \|r z\|$
229	221	abscld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r z\| \in ℝ$
230	229 190	ltnled	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (\|r z\| < r + d \leftrightarrow \neg r + d \leq \|r z\|)$
231	228 230	mpbird	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|r z\| < r + d$
232	202 231	eqbrtrrd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r \|z\| < r + d$
233	184 190 186	ltmuldiv2d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (r \|z\| < r + d \leftrightarrow \|z\| < \frac{r + d}{r})$
234	232 233	mpbid	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|z\| < \frac{r + d}{r}$
235		flltp1	$⊢ \frac{r + d}{r} \in ℝ \to \frac{r + d}{r} < ⌊\frac{r + d}{r}⌋ + 1$
236	191 235	syl	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \frac{r + d}{r} < ⌊\frac{r + d}{r}⌋ + 1$
237	184 191 194 234 236	lttrd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|z\| < ⌊\frac{r + d}{r}⌋ + 1$
238	184 194 237	ltled	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|z\| \leq ⌊\frac{r + d}{r}⌋ + 1$
239	182 184 194 196 238	letrd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|ℜ (z)\| \leq ⌊\frac{r + d}{r}⌋ + 1$
240	180	zred	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℜ (z) \in ℝ$
241	240 194	absled	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (\|ℜ (z)\| \leq ⌊\frac{r + d}{r}⌋ + 1 \leftrightarrow (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℜ (z) \land ℜ (z) \leq ⌊\frac{r + d}{r}⌋ + 1))$
242	239 241	mpbid	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℜ (z) \land ℜ (z) \leq ⌊\frac{r + d}{r}⌋ + 1)$
243	193	znegcld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to - (⌊\frac{r + d}{r}⌋ + 1) \in ℤ$
244		elfz	$⊢ (ℜ (z) \in ℤ \land - (⌊\frac{r + d}{r}⌋ + 1) \in ℤ \land ⌊\frac{r + d}{r}⌋ + 1 \in ℤ) \to (ℜ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \leftrightarrow (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℜ (z) \land ℜ (z) \leq ⌊\frac{r + d}{r}⌋ + 1))$
245	180 243 193 244	syl3anc	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (ℜ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \leftrightarrow (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℜ (z) \land ℜ (z) \leq ⌊\frac{r + d}{r}⌋ + 1))$
246	242 245	mpbird	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℜ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1)$
247	178	simp3bi	$⊢ z \in ℤ [i] \to ℑ (z) \in ℤ$
248	247	ad2antlr	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℑ (z) \in ℤ$
249	248	zcnd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℑ (z) \in ℂ$
250	249	abscld	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|ℑ (z)\| \in ℝ$
251		absimle	$⊢ z \in ℂ \to \|ℑ (z)\| \leq \|z\|$
252	183 251	syl	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|ℑ (z)\| \leq \|z\|$
253	250 184 194 252 238	letrd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \|ℑ (z)\| \leq ⌊\frac{r + d}{r}⌋ + 1$
254	248	zred	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℑ (z) \in ℝ$
255	254 194	absled	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (\|ℑ (z)\| \leq ⌊\frac{r + d}{r}⌋ + 1 \leftrightarrow (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℑ (z) \land ℑ (z) \leq ⌊\frac{r + d}{r}⌋ + 1))$
256	253 255	mpbid	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℑ (z) \land ℑ (z) \leq ⌊\frac{r + d}{r}⌋ + 1)$
257		elfz	$⊢ (ℑ (z) \in ℤ \land - (⌊\frac{r + d}{r}⌋ + 1) \in ℤ \land ⌊\frac{r + d}{r}⌋ + 1 \in ℤ) \to (ℑ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \leftrightarrow (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℑ (z) \land ℑ (z) \leq ⌊\frac{r + d}{r}⌋ + 1))$
258	248 243 193 257	syl3anc	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to (ℑ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \leftrightarrow (- (⌊\frac{r + d}{r}⌋ + 1) \leq ℑ (z) \land ℑ (z) \leq ⌊\frac{r + d}{r}⌋ + 1))$
259	256 258	mpbird	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to ℑ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1)$
260	183	replimd	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to z = ℜ (z) + i ℑ (z)$
261	260	oveq2d	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to r z = r (ℜ (z) + i ℑ (z))$
262		oveq1	$⊢ a = ℜ (z) \to a + i b = ℜ (z) + i b$
263	262	oveq2d	$⊢ a = ℜ (z) \to r (a + i b) = r (ℜ (z) + i b)$
264	263	eqeq2d	$⊢ a = ℜ (z) \to (r z = r (a + i b) \leftrightarrow r z = r (ℜ (z) + i b))$
265		oveq2	$⊢ b = ℑ (z) \to i b = i ℑ (z)$
266	265	oveq2d	$⊢ b = ℑ (z) \to ℜ (z) + i b = ℜ (z) + i ℑ (z)$
267	266	oveq2d	$⊢ b = ℑ (z) \to r (ℜ (z) + i b) = r (ℜ (z) + i ℑ (z))$
268	267	eqeq2d	$⊢ b = ℑ (z) \to (r z = r (ℜ (z) + i b) \leftrightarrow r z = r (ℜ (z) + i ℑ (z)))$
269	264 268	rspc2ev	$⊢ (ℜ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \land ℑ (z) \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \land r z = r (ℜ (z) + i ℑ (z))) \to \exists a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \exists b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) r z = r (a + i b)$
270	246 259 261 269	syl3anc	$⊢ ((((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \land (r z ball (abs \circ -) r) \cap X \neq \emptyset) \to \exists a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \exists b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) r z = r (a + i b)$
271	270	ex	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to ((r z ball (abs \circ -) r) \cap X \neq \emptyset \to \exists a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \exists b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) r z = r (a + i b))$
272	170 171	elrnmpo	$⊢ r z \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) \leftrightarrow \exists a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \exists b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) r z = r (a + i b)$
273	271 272	imbitrrdi	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to ((r z ball (abs \circ -) r) \cap X \neq \emptyset \to r z \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)))$
274	156	ineq1d	$⊢ x = r z \to (x ball (abs \circ -) r) \cap X = (r z ball (abs \circ -) r) \cap X$
275	274	neeq1d	$⊢ x = r z \to ((x ball (abs \circ -) r) \cap X \neq \emptyset \leftrightarrow (r z ball (abs \circ -) r) \cap X \neq \emptyset)$
276		eleq1	$⊢ x = r z \to (x \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) \leftrightarrow r z \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)))$
277	275 276	imbi12d	$⊢ x = r z \to (((x ball (abs \circ -) r) \cap X \neq \emptyset \to x \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))) \leftrightarrow ((r z ball (abs \circ -) r) \cap X \neq \emptyset \to r z \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))))$
278	273 277	syl5ibrcom	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land z \in ℤ [i]) \to (x = r z \to ((x ball (abs \circ -) r) \cap X \neq \emptyset \to x \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))))$
279	278	rexlimdva	$⊢ ((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \to (\exists z \in ℤ [i] x = r z \to ((x ball (abs \circ -) r) \cap X \neq \emptyset \to x \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))))$
280	177 279	biimtrid	$⊢ ((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \to (x \in ran (z \in ℤ [i] ⟼ r z) \to ((x ball (abs \circ -) r) \cap X \neq \emptyset \to x \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))))$
281	280	3imp	$⊢ (((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \land x \in ran (z \in ℤ [i] ⟼ r z) \land (x ball (abs \circ -) r) \cap X \neq \emptyset) \to x \in ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))$
282	281	rabssdv	$⊢ ((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \to \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \subseteq ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))$
283		ssfi	$⊢ (ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b)) \in Fin \land \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \subseteq ran (a \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1), b \in (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) ⟼ r (a + i b))) \to \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin$
284	176 282 283	sylancr	$⊢ ((D \in Bnd (X) \land r \in ℝ^{+}) \land (d \in ℝ \land X \subseteq 0 ball (abs \circ -) d)) \to \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin$
285	166 284	rexlimddv	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin$
286		iuneq1	$⊢ y = ran (z \in ℤ [i] ⟼ r z) \to ⋃_{x \in y} (x ball (abs \circ -) r) = ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r)$
287	286	sseq2d	$⊢ y = ran (z \in ℤ [i] ⟼ r z) \to (X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \leftrightarrow X \subseteq ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r))$
288		rabeq	$⊢ y = ran (z \in ℤ [i] ⟼ r z) \to \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} = \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\}$
289	288	eleq1d	$⊢ y = ran (z \in ℤ [i] ⟼ r z) \to (\{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin \leftrightarrow \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin)$
290	287 289	anbi12d	$⊢ y = ran (z \in ℤ [i] ⟼ r z) \to ((X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \land \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin) \leftrightarrow (X \subseteq ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r) \land \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin))$
291	290	rspcev	$⊢ (ran (z \in ℤ [i] ⟼ r z) \in 𝒫 ℂ \land (X \subseteq ⋃_{x \in ran (z \in ℤ [i] ⟼ r z)} (x ball (abs \circ -) r) \land \{x \in ran (z \in ℤ [i] ⟼ r z) \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin)) \to \exists y \in 𝒫 ℂ (X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \land \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin)$
292	12 162 285 291	syl12anc	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to \exists y \in 𝒫 ℂ (X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \land \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin)$
293	292	ralrimiva	$⊢ D \in Bnd (X) \to \forall r \in ℝ^{+} \exists y \in 𝒫 ℂ (X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \land \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin)$
294	1	sstotbnd3	$⊢ (abs \circ - \in Met (ℂ) \land X \subseteq ℂ) \to (D \in TotBnd (X) \leftrightarrow \forall r \in ℝ^{+} \exists y \in 𝒫 ℂ (X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \land \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin))$
295	13 15 294	sylancr	$⊢ D \in Bnd (X) \to (D \in TotBnd (X) \leftrightarrow \forall r \in ℝ^{+} \exists y \in 𝒫 ℂ (X \subseteq ⋃_{x \in y} (x ball (abs \circ -) r) \land \{x \in y \| (x ball (abs \circ -) r) \cap X \neq \emptyset\} \in Fin))$
296	293 295	mpbird	$⊢ D \in Bnd (X) \to D \in TotBnd (X)$
297	2 296	impbii	$⊢ D \in TotBnd (X) \leftrightarrow D \in Bnd (X)$

Metamath Proof Explorer

Theorem cntotbnd

Proof