cnheibor

Description: Heine-Borel theorem for complex numbers. A subset of CC is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	cnheibor.2	$⊢ J = TopOpen (ℂ_{fld})$
	cnheibor.3	$⊢ T = J ↾_{𝑡} X$
Assertion	cnheibor	$⊢ X \subseteq ℂ \to (T \in Comp \leftrightarrow (X \in Clsd (J) \land \exists r \in ℝ \forall x \in X \|x\| \leq r))$

Proof

Step	Hyp	Ref	Expression
1		cnheibor.2	$⊢ J = TopOpen (ℂ_{fld})$
2		cnheibor.3	$⊢ T = J ↾_{𝑡} X$
3	1	cnfldhaus	$⊢ J \in Haus$
4		simpl	$⊢ (X \subseteq ℂ \land T \in Comp) \to X \subseteq ℂ$
5		simpr	$⊢ (X \subseteq ℂ \land T \in Comp) \to T \in Comp$
6	2 5	eqeltrrid	$⊢ (X \subseteq ℂ \land T \in Comp) \to J ↾_{𝑡} X \in Comp$
7	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
8	7	toponunii	$⊢ ℂ = ⋃ J$
9	8	hauscmp	$⊢ (J \in Haus \land X \subseteq ℂ \land J ↾_{𝑡} X \in Comp) \to X \in Clsd (J)$
10	3 4 6 9	mp3an2i	$⊢ (X \subseteq ℂ \land T \in Comp) \to X \in Clsd (J)$
11	1	cnfldtop	$⊢ J \in Top$
12	8	restuni	$⊢ (J \in Top \land X \subseteq ℂ) \to X = ⋃ (J ↾_{𝑡} X)$
13	11 4 12	sylancr	$⊢ (X \subseteq ℂ \land T \in Comp) \to X = ⋃ (J ↾_{𝑡} X)$
14	2	unieqi	$⊢ ⋃ T = ⋃ (J ↾_{𝑡} X)$
15	13 14	eqtr4di	$⊢ (X \subseteq ℂ \land T \in Comp) \to X = ⋃ T$
16	15	eleq2d	$⊢ (X \subseteq ℂ \land T \in Comp) \to (x \in X \leftrightarrow x \in ⋃ T)$
17	16	biimpar	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in ⋃ T) \to x \in X$
18		cnex	$⊢ ℂ \in V$
19		ssexg	$⊢ (X \subseteq ℂ \land ℂ \in V) \to X \in V$
20	4 18 19	sylancl	$⊢ (X \subseteq ℂ \land T \in Comp) \to X \in V$
21	20	adantr	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to X \in V$
22		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
23		0cnd	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to 0 \in ℂ$
24	4	sselda	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to x \in ℂ$
25	24	abscld	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \|x\| \in ℝ$
26		peano2re	$⊢ \|x\| \in ℝ \to \|x\| + 1 \in ℝ$
27	25 26	syl	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \|x\| + 1 \in ℝ$
28	27	rexrd	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \|x\| + 1 \in ℝ^{*}$
29	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
30	29	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land \|x\| + 1 \in ℝ^{*}) \to 0 ball (abs \circ -) (\|x\| + 1) \in J$
31	22 23 28 30	mp3an2i	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to 0 ball (abs \circ -) (\|x\| + 1) \in J$
32		elrestr	$⊢ (J \in Top \land X \in V \land 0 ball (abs \circ -) (\|x\| + 1) \in J) \to (0 ball (abs \circ -) (\|x\| + 1)) \cap X \in (J ↾_{𝑡} X)$
33	11 21 31 32	mp3an2i	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to (0 ball (abs \circ -) (\|x\| + 1)) \cap X \in (J ↾_{𝑡} X)$
34	33 2	eleqtrrdi	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to (0 ball (abs \circ -) (\|x\| + 1)) \cap X \in T$
35		0cn	$⊢ 0 \in ℂ$
36		eqid	$⊢ abs \circ - = abs \circ -$
37	36	cnmetdval	$⊢ (0 \in ℂ \land x \in ℂ) \to 0 (abs \circ -) x = \|0 - x\|$
38	35 37	mpan	$⊢ x \in ℂ \to 0 (abs \circ -) x = \|0 - x\|$
39		df-neg	$⊢ - x = 0 - x$
40	39	fveq2i	$⊢ \|- x\| = \|0 - x\|$
41		absneg	$⊢ x \in ℂ \to \|- x\| = \|x\|$
42	40 41	eqtr3id	$⊢ x \in ℂ \to \|0 - x\| = \|x\|$
43	38 42	eqtrd	$⊢ x \in ℂ \to 0 (abs \circ -) x = \|x\|$
44	24 43	syl	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to 0 (abs \circ -) x = \|x\|$
45	25	ltp1d	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \|x\| < \|x\| + 1$
46	44 45	eqbrtrd	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to 0 (abs \circ -) x < \|x\| + 1$
47		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land \|x\| + 1 \in ℝ^{*}) \to (x \in (0 ball (abs \circ -) (\|x\| + 1)) \leftrightarrow (x \in ℂ \land 0 (abs \circ -) x < \|x\| + 1))$
48	22 23 28 47	mp3an2i	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to (x \in (0 ball (abs \circ -) (\|x\| + 1)) \leftrightarrow (x \in ℂ \land 0 (abs \circ -) x < \|x\| + 1))$
49	24 46 48	mpbir2and	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to x \in (0 ball (abs \circ -) (\|x\| + 1))$
50		simpr	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to x \in X$
51	49 50	elind	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to x \in ((0 ball (abs \circ -) (\|x\| + 1)) \cap X)$
52	24	absge0d	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to 0 \leq \|x\|$
53	25 52	ge0p1rpd	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \|x\| + 1 \in ℝ^{+}$
54		eqid	$⊢ (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) (\|x\| + 1)) \cap X$
55		oveq2	$⊢ r = \|x\| + 1 \to 0 ball (abs \circ -) r = 0 ball (abs \circ -) (\|x\| + 1)$
56	55	ineq1d	$⊢ r = \|x\| + 1 \to (0 ball (abs \circ -) r) \cap X = (0 ball (abs \circ -) (\|x\| + 1)) \cap X$
57	56	rspceeqv	$⊢ (\|x\| + 1 \in ℝ^{+} \land (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) (\|x\| + 1)) \cap X) \to \exists r \in ℝ^{+} (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) r) \cap X$
58	53 54 57	sylancl	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \exists r \in ℝ^{+} (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) r) \cap X$
59		eleq2	$⊢ u = (0 ball (abs \circ -) (\|x\| + 1)) \cap X \to (x \in u \leftrightarrow x \in ((0 ball (abs \circ -) (\|x\| + 1)) \cap X))$
60		eqeq1	$⊢ u = (0 ball (abs \circ -) (\|x\| + 1)) \cap X \to (u = (0 ball (abs \circ -) r) \cap X \leftrightarrow (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) r) \cap X)$
61	60	rexbidv	$⊢ u = (0 ball (abs \circ -) (\|x\| + 1)) \cap X \to (\exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X \leftrightarrow \exists r \in ℝ^{+} (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) r) \cap X)$
62	59 61	anbi12d	$⊢ u = (0 ball (abs \circ -) (\|x\| + 1)) \cap X \to ((x \in u \land \exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X) \leftrightarrow (x \in ((0 ball (abs \circ -) (\|x\| + 1)) \cap X) \land \exists r \in ℝ^{+} (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) r) \cap X))$
63	62	rspcev	$⊢ ((0 ball (abs \circ -) (\|x\| + 1)) \cap X \in T \land (x \in ((0 ball (abs \circ -) (\|x\| + 1)) \cap X) \land \exists r \in ℝ^{+} (0 ball (abs \circ -) (\|x\| + 1)) \cap X = (0 ball (abs \circ -) r) \cap X)) \to \exists u \in T (x \in u \land \exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X)$
64	34 51 58 63	syl12anc	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in X) \to \exists u \in T (x \in u \land \exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X)$
65	17 64	syldan	$⊢ ((X \subseteq ℂ \land T \in Comp) \land x \in ⋃ T) \to \exists u \in T (x \in u \land \exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X)$
66	65	ralrimiva	$⊢ (X \subseteq ℂ \land T \in Comp) \to \forall x \in ⋃ T \exists u \in T (x \in u \land \exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X)$
67		eqid	$⊢ ⋃ T = ⋃ T$
68		oveq2	$⊢ r = f (u) \to 0 ball (abs \circ -) r = 0 ball (abs \circ -) f (u)$
69	68	ineq1d	$⊢ r = f (u) \to (0 ball (abs \circ -) r) \cap X = (0 ball (abs \circ -) f (u)) \cap X$
70	69	eqeq2d	$⊢ r = f (u) \to (u = (0 ball (abs \circ -) r) \cap X \leftrightarrow u = (0 ball (abs \circ -) f (u)) \cap X)$
71	67 70	cmpcovf	$⊢ (T \in Comp \land \forall x \in ⋃ T \exists u \in T (x \in u \land \exists r \in ℝ^{+} u = (0 ball (abs \circ -) r) \cap X)) \to \exists s \in (𝒫 T \cap Fin) (⋃ T = ⋃ s \land \exists f (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X))$
72	5 66 71	syl2anc	$⊢ (X \subseteq ℂ \land T \in Comp) \to \exists s \in (𝒫 T \cap Fin) (⋃ T = ⋃ s \land \exists f (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X))$
73	15	ad4antr	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to X = ⋃ T$
74		simpllr	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to ⋃ T = ⋃ s$
75	73 74	eqtrd	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to X = ⋃ s$
76	75	eleq2d	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to (x \in X \leftrightarrow x \in ⋃ s)$
77		eluni2	$⊢ x \in ⋃ s \leftrightarrow \exists z \in s x \in z$
78	76 77	bitrdi	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to (x \in X \leftrightarrow \exists z \in s x \in z)$
79		elssuni	$⊢ z \in s \to z \subseteq ⋃ s$
80	79	ad2antrl	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to z \subseteq ⋃ s$
81	75	adantr	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to X = ⋃ s$
82	80 81	sseqtrrd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to z \subseteq X$
83		simp-6l	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to X \subseteq ℂ$
84	82 83	sstrd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to z \subseteq ℂ$
85		simprr	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to x \in z$
86	84 85	sseldd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to x \in ℂ$
87	86	abscld	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to \|x\| \in ℝ$
88		simplrl	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to r \in ℝ$
89		simprl	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to f : s ⟶ ℝ^{+}$
90	89	ad2antrr	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to f : s ⟶ ℝ^{+}$
91		simprl	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to z \in s$
92	90 91	ffvelcdmd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to f (z) \in ℝ^{+}$
93	92	rpred	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to f (z) \in ℝ$
94	86 43	syl	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to 0 (abs \circ -) x = \|x\|$
95		id	$⊢ u = z \to u = z$
96		fveq2	$⊢ u = z \to f (u) = f (z)$
97	96	oveq2d	$⊢ u = z \to 0 ball (abs \circ -) f (u) = 0 ball (abs \circ -) f (z)$
98	97	ineq1d	$⊢ u = z \to (0 ball (abs \circ -) f (u)) \cap X = (0 ball (abs \circ -) f (z)) \cap X$
99	95 98	eqeq12d	$⊢ u = z \to (u = (0 ball (abs \circ -) f (u)) \cap X \leftrightarrow z = (0 ball (abs \circ -) f (z)) \cap X)$
100		simprr	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X$
101	100	ad2antrr	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X$
102	99 101 91	rspcdva	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to z = (0 ball (abs \circ -) f (z)) \cap X$
103	85 102	eleqtrd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to x \in ((0 ball (abs \circ -) f (z)) \cap X)$
104	103	elin1d	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to x \in (0 ball (abs \circ -) f (z))$
105		0cnd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to 0 \in ℂ$
106	92	rpxrd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to f (z) \in ℝ^{*}$
107		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land f (z) \in ℝ^{*}) \to (x \in (0 ball (abs \circ -) f (z)) \leftrightarrow (x \in ℂ \land 0 (abs \circ -) x < f (z)))$
108	22 105 106 107	mp3an2i	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to (x \in (0 ball (abs \circ -) f (z)) \leftrightarrow (x \in ℂ \land 0 (abs \circ -) x < f (z)))$
109	104 108	mpbid	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to (x \in ℂ \land 0 (abs \circ -) x < f (z))$
110	109	simprd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to 0 (abs \circ -) x < f (z)$
111	94 110	eqbrtrrd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to \|x\| < f (z)$
112	96	breq1d	$⊢ u = z \to (f (u) \leq r \leftrightarrow f (z) \leq r)$
113		simplrr	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to \forall u \in s f (u) \leq r$
114	112 113 91	rspcdva	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to f (z) \leq r$
115	87 93 88 111 114	ltletrd	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to \|x\| < r$
116	87 88 115	ltled	$⊢ ((((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \land (z \in s \land x \in z)) \to \|x\| \leq r$
117	116	rexlimdvaa	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to (\exists z \in s x \in z \to \|x\| \leq r)$
118	78 117	sylbid	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to (x \in X \to \|x\| \leq r)$
119	118	ralrimiv	$⊢ (((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \land (r \in ℝ \land \forall u \in s f (u) \leq r)) \to \forall x \in X \|x\| \leq r$
120		simpllr	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to s \in (𝒫 T \cap Fin)$
121	120	elin2d	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to s \in Fin$
122		ffvelcdm	$⊢ (f : s ⟶ ℝ^{+} \land u \in s) \to f (u) \in ℝ^{+}$
123	122	rpred	$⊢ (f : s ⟶ ℝ^{+} \land u \in s) \to f (u) \in ℝ$
124	123	ralrimiva	$⊢ f : s ⟶ ℝ^{+} \to \forall u \in s f (u) \in ℝ$
125	124	ad2antrl	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to \forall u \in s f (u) \in ℝ$
126		fimaxre3	$⊢ (s \in Fin \land \forall u \in s f (u) \in ℝ) \to \exists r \in ℝ \forall u \in s f (u) \leq r$
127	121 125 126	syl2anc	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to \exists r \in ℝ \forall u \in s f (u) \leq r$
128	119 127	reximddv	$⊢ ((((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \land (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to \exists r \in ℝ \forall x \in X \|x\| \leq r$
129	128	ex	$⊢ (((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \to ((f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X) \to \exists r \in ℝ \forall x \in X \|x\| \leq r)$
130	129	exlimdv	$⊢ (((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \land ⋃ T = ⋃ s) \to (\exists f (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X) \to \exists r \in ℝ \forall x \in X \|x\| \leq r)$
131	130	expimpd	$⊢ ((X \subseteq ℂ \land T \in Comp) \land s \in (𝒫 T \cap Fin)) \to ((⋃ T = ⋃ s \land \exists f (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to \exists r \in ℝ \forall x \in X \|x\| \leq r)$
132	131	rexlimdva	$⊢ (X \subseteq ℂ \land T \in Comp) \to (\exists s \in (𝒫 T \cap Fin) (⋃ T = ⋃ s \land \exists f (f : s ⟶ ℝ^{+} \land \forall u \in s u = (0 ball (abs \circ -) f (u)) \cap X)) \to \exists r \in ℝ \forall x \in X \|x\| \leq r)$
133	72 132	mpd	$⊢ (X \subseteq ℂ \land T \in Comp) \to \exists r \in ℝ \forall x \in X \|x\| \leq r$
134	10 133	jca	$⊢ (X \subseteq ℂ \land T \in Comp) \to (X \in Clsd (J) \land \exists r \in ℝ \forall x \in X \|x\| \leq r)$
135		eqid	$⊢ (y \in ℝ, z \in ℝ ⟼ y + i z) = (y \in ℝ, z \in ℝ ⟼ y + i z)$
136		eqid	$⊢ (y \in ℝ, z \in ℝ ⟼ y + i z) [[- r, r] \times [- r, r]] = (y \in ℝ, z \in ℝ ⟼ y + i z) [[- r, r] \times [- r, r]]$
137	1 2 135 136	cnheiborlem	$⊢ (X \in Clsd (J) \land (r \in ℝ \land \forall x \in X \|x\| \leq r)) \to T \in Comp$
138	137	rexlimdvaa	$⊢ X \in Clsd (J) \to (\exists r \in ℝ \forall x \in X \|x\| \leq r \to T \in Comp)$
139	138	imp	$⊢ (X \in Clsd (J) \land \exists r \in ℝ \forall x \in X \|x\| \leq r) \to T \in Comp$
140	139	adantl	$⊢ (X \subseteq ℂ \land (X \in Clsd (J) \land \exists r \in ℝ \forall x \in X \|x\| \leq r)) \to T \in Comp$
141	134 140	impbida	$⊢ X \subseteq ℂ \to (T \in Comp \leftrightarrow (X \in Clsd (J) \land \exists r \in ℝ \forall x \in X \|x\| \leq r))$

Metamath Proof Explorer

Theorem cnheibor

Proof