zcld

Description: The integers are a closed set in the topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)

		Ref	Expression
	Hypothesis	zcld.1	$⊢ J = topGen (ran (.))$
	Assertion	zcld	$⊢ ℤ \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		zcld.1	$⊢ J = topGen (ran (.))$
2		eliun	$⊢ y \in ⋃_{x \in ℤ} (x, x + 1) \leftrightarrow \exists x \in ℤ y \in (x, x + 1)$
3		elioore	$⊢ y \in (x, x + 1) \to y \in ℝ$
4	3	adantl	$⊢ (x \in ℤ \land y \in (x, x + 1)) \to y \in ℝ$
5		eliooord	$⊢ y \in (x, x + 1) \to (x < y \land y < x + 1)$
6		btwnnz	$⊢ (x \in ℤ \land x < y \land y < x + 1) \to \neg y \in ℤ$
7	6	3expb	$⊢ (x \in ℤ \land (x < y \land y < x + 1)) \to \neg y \in ℤ$
8	5 7	sylan2	$⊢ (x \in ℤ \land y \in (x, x + 1)) \to \neg y \in ℤ$
9	4 8	eldifd	$⊢ (x \in ℤ \land y \in (x, x + 1)) \to y \in (ℝ ∖ ℤ)$
10	9	rexlimiva	$⊢ \exists x \in ℤ y \in (x, x + 1) \to y \in (ℝ ∖ ℤ)$
11		eldifi	$⊢ y \in (ℝ ∖ ℤ) \to y \in ℝ$
12	11	flcld	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ \in ℤ$
13	12	zred	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ \in ℝ$
14		flle	$⊢ y \in ℝ \to ⌊y⌋ \leq y$
15	11 14	syl	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ \leq y$
16		eldifn	$⊢ y \in (ℝ ∖ ℤ) \to \neg y \in ℤ$
17		nelne2	$⊢ (⌊y⌋ \in ℤ \land \neg y \in ℤ) \to ⌊y⌋ \neq y$
18	12 16 17	syl2anc	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ \neq y$
19	18	necomd	$⊢ y \in (ℝ ∖ ℤ) \to y \neq ⌊y⌋$
20	13 11 15 19	leneltd	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ < y$
21		flltp1	$⊢ y \in ℝ \to y < ⌊y⌋ + 1$
22	11 21	syl	$⊢ y \in (ℝ ∖ ℤ) \to y < ⌊y⌋ + 1$
23	13	rexrd	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ \in ℝ^{*}$
24		peano2re	$⊢ ⌊y⌋ \in ℝ \to ⌊y⌋ + 1 \in ℝ$
25	13 24	syl	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ + 1 \in ℝ$
26	25	rexrd	$⊢ y \in (ℝ ∖ ℤ) \to ⌊y⌋ + 1 \in ℝ^{*}$
27		elioo2	$⊢ (⌊y⌋ \in ℝ^{} \land ⌊y⌋ + 1 \in ℝ^{}) \to (y \in (⌊y⌋, ⌊y⌋ + 1) \leftrightarrow (y \in ℝ \land ⌊y⌋ < y \land y < ⌊y⌋ + 1))$
28	23 26 27	syl2anc	$⊢ y \in (ℝ ∖ ℤ) \to (y \in (⌊y⌋, ⌊y⌋ + 1) \leftrightarrow (y \in ℝ \land ⌊y⌋ < y \land y < ⌊y⌋ + 1))$
29	11 20 22 28	mpbir3and	$⊢ y \in (ℝ ∖ ℤ) \to y \in (⌊y⌋, ⌊y⌋ + 1)$
30		id	$⊢ x = ⌊y⌋ \to x = ⌊y⌋$
31		oveq1	$⊢ x = ⌊y⌋ \to x + 1 = ⌊y⌋ + 1$
32	30 31	oveq12d	$⊢ x = ⌊y⌋ \to (x, x + 1) = (⌊y⌋, ⌊y⌋ + 1)$
33	32	eleq2d	$⊢ x = ⌊y⌋ \to (y \in (x, x + 1) \leftrightarrow y \in (⌊y⌋, ⌊y⌋ + 1))$
34	33	rspcev	$⊢ (⌊y⌋ \in ℤ \land y \in (⌊y⌋, ⌊y⌋ + 1)) \to \exists x \in ℤ y \in (x, x + 1)$
35	12 29 34	syl2anc	$⊢ y \in (ℝ ∖ ℤ) \to \exists x \in ℤ y \in (x, x + 1)$
36	10 35	impbii	$⊢ \exists x \in ℤ y \in (x, x + 1) \leftrightarrow y \in (ℝ ∖ ℤ)$
37	2 36	bitri	$⊢ y \in ⋃_{x \in ℤ} (x, x + 1) \leftrightarrow y \in (ℝ ∖ ℤ)$
38	37	eqriv	$⊢ ⋃_{x \in ℤ} (x, x + 1) = ℝ ∖ ℤ$
39		retop	$⊢ topGen (ran (.)) \in Top$
40	1 39	eqeltri	$⊢ J \in Top$
41		iooretop	$⊢ (x, x + 1) \in topGen (ran (.))$
42	41 1	eleqtrri	$⊢ (x, x + 1) \in J$
43	42	rgenw	$⊢ \forall x \in ℤ (x, x + 1) \in J$
44		iunopn	$⊢ (J \in Top \land \forall x \in ℤ (x, x + 1) \in J) \to ⋃_{x \in ℤ} (x, x + 1) \in J$
45	40 43 44	mp2an	$⊢ ⋃_{x \in ℤ} (x, x + 1) \in J$
46	38 45	eqeltrri	$⊢ ℝ ∖ ℤ \in J$
47		zssre	$⊢ ℤ \subseteq ℝ$
48		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
49	1	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
50	48 49	eqtr4i	$⊢ ℝ = ⋃ J$
51	50	iscld2	$⊢ (J \in Top \land ℤ \subseteq ℝ) \to (ℤ \in Clsd (J) \leftrightarrow ℝ ∖ ℤ \in J)$
52	40 47 51	mp2an	$⊢ ℤ \in Clsd (J) \leftrightarrow ℝ ∖ ℤ \in J$
53	46 52	mpbir	$⊢ ℤ \in Clsd (J)$

Metamath Proof Explorer

Theorem zcld

Proof