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	mulid2i	$⊢ 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	mulid1d	$⊢ (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	syl6ibr	$⊢ (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		simpl	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to D \in Bnd (X)$
164		0cn	$⊢ 0 \in ℂ$
165	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)$
166	13 164 165	mp2an	$⊢ D \in Bnd (X) \leftrightarrow \exists d \in ℝ X \subseteq 0 ball (abs \circ -) d$
167	163 166	sylib	$⊢ (D \in Bnd (X) \land r \in ℝ^{+}) \to \exists d \in ℝ X \subseteq 0 ball (abs \circ -) d$
168		fzfi	$⊢ (- (⌊\frac{r + d}{r}⌋ + 1) \dots ⌊\frac{r + d}{r}⌋ + 1) \in Fin$
169		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$
170	168 168 169	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$
171		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))$
172		ovex	$⊢ r (a + i b) \in V$
173	171 172	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))$
174		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))$
175	173 174	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))$
176		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$
177	170 175 176	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$
178	155 153	elrnmpti	$⊢ x \in ran (z \in ℤ [i] ⟼ r z) \leftrightarrow \exists z \in ℤ [i] x = r z$
179		elgz	$⊢ z \in ℤ [i] \leftrightarrow (z \in ℂ \land ℜ (z) \in ℤ \land ℑ (z) \in ℤ)$
180	179	simp2bi	$⊢ z \in ℤ [i] \to ℜ (z) \in ℤ$
181	180	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 ℤ$
182	181	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 ℂ$
183	182	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 ℝ$
184	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 ℂ$
185	184	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 ℝ$
186		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 ℝ^{+}$
187	186	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 ℝ^{+}$
188	187	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 ℝ$
189		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 ℝ$
190	189	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 ℝ$
191	188 190	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 ℝ$
192	191 187	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 ℝ$
193	192	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 ℤ$
194	193	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 ℤ$
195	194	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 ℝ$
196		absrele	$⊢ z \in ℂ \to \|ℜ (z)\| \leq \|z\|$
197	184 196	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\|$
198	187	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 ℂ$
199	198 184	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\|$
200	187	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$
201	188 200	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$
202	201	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\|$
203	199 202	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\|$
204		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$
205		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)$
206	204 205	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)$
207	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 (ℂ)$
208	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 ℂ$
209	164	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 ℂ$
210	186	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 ℝ^{*}$
211	189	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 ℝ^{*}$
212		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$
213	212	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)))$
214	213	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)$
215	207 208 209 210 211 214	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)$
216		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$
217	206 215 216	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)$
218	217	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)$
219	218	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$
220		rexadd	$⊢ (r \in ℝ \land d \in ℝ) \to r +_{𝑒} d = r + d$
221	188 190 220	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$
222	208	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 ℂ$
223	123	cnmetdval	$⊢ (r z \in ℂ \land 0 \in ℂ) \to r z (abs \circ -) 0 = \|r z - 0\|$
224	222 164 223	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\|$
225	222	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$
226	225	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\|$
227	224 226	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\|$
228	221 227	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\|)$
229	219 228	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\|$
230	222	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 ℝ$
231	230 191	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\|)$
232	229 231	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$
233	203 232	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$
234	185 191 187	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})$
235	233 234	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}$
236		flltp1	$⊢ \frac{r + d}{r} \in ℝ \to \frac{r + d}{r} < ⌊\frac{r + d}{r}⌋ + 1$
237	192 236	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$
238	185 192 195 235 237	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$
239	185 195 238	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$
240	183 185 195 197 239	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$
241	181	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 ℝ$
242	241 195	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))$
243	240 242	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)$
244	194	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 ℤ$
245		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))$
246	181 244 194 245	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))$
247	243 246	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)$
248	179	simp3bi	$⊢ z \in ℤ [i] \to ℑ (z) \in ℤ$
249	248	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 ℤ$
250	249	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 ℂ$
251	250	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 ℝ$
252		absimle	$⊢ z \in ℂ \to \|ℑ (z)\| \leq \|z\|$
253	184 252	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\|$
254	251 185 195 253 239	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$
255	249	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 ℝ$
256	255 195	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))$
257	254 256	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)$
258		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))$
259	249 244 194 258	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))$
260	257 259	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)$
261	184	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)$
262	261	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))$
263		oveq1	$⊢ a = ℜ (z) \to a + i b = ℜ (z) + i b$
264	263	oveq2d	$⊢ a = ℜ (z) \to r (a + i b) = r (ℜ (z) + i b)$
265	264	eqeq2d	$⊢ a = ℜ (z) \to (r z = r (a + i b) \leftrightarrow r z = r (ℜ (z) + i b))$
266		oveq2	$⊢ b = ℑ (z) \to i b = i ℑ (z)$
267	266	oveq2d	$⊢ b = ℑ (z) \to ℜ (z) + i b = ℜ (z) + i ℑ (z)$
268	267	oveq2d	$⊢ b = ℑ (z) \to r (ℜ (z) + i b) = r (ℜ (z) + i ℑ (z))$
269	268	eqeq2d	$⊢ b = ℑ (z) \to (r z = r (ℜ (z) + i b) \leftrightarrow r z = r (ℜ (z) + i ℑ (z)))$
270	265 269	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)$
271	247 260 262 270	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)$
272	271	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))$
273	171 172	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)$
274	272 273	syl6ibr	$⊢ (((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)))$
275	156	ineq1d	$⊢ x = r z \to (x ball (abs \circ -) r) \cap X = (r z ball (abs \circ -) r) \cap X$
276	275	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)$
277		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)))$
278	276 277	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))))$
279	274 278	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))))$
280	279	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))))$
281	178 280	syl5bi	$⊢ ((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))))$
282	281	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))$
283	282	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))$
284		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$
285	177 283 284	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$
286	167 285	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$
287		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)$
288	287	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))$
289		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\}$
290	289	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)$
291	288 290	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))$
292	291	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)$
293	12 162 286 292	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)$
294	293	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)$
295	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))$
296	13 15 295	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))$
297	294 296	mpbird	$⊢ D \in Bnd (X) \to D \in TotBnd (X)$
298	2 297	impbii	$⊢ D \in TotBnd (X) \leftrightarrow D \in Bnd (X)$

Metamath Proof Explorer

Theorem cntotbnd

Proof