Description: The integers are a closed set in the topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | zcld.1 | |
|
Assertion | zcld | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcld.1 | |
|
2 | eliun | |
|
3 | elioore | |
|
4 | 3 | adantl | |
5 | eliooord | |
|
6 | btwnnz | |
|
7 | 6 | 3expb | |
8 | 5 7 | sylan2 | |
9 | 4 8 | eldifd | |
10 | 9 | rexlimiva | |
11 | eldifi | |
|
12 | 11 | flcld | |
13 | 12 | zred | |
14 | flle | |
|
15 | 11 14 | syl | |
16 | eldifn | |
|
17 | nelne2 | |
|
18 | 12 16 17 | syl2anc | |
19 | 18 | necomd | |
20 | 13 11 15 19 | leneltd | |
21 | flltp1 | |
|
22 | 11 21 | syl | |
23 | 13 | rexrd | |
24 | peano2re | |
|
25 | 13 24 | syl | |
26 | 25 | rexrd | |
27 | elioo2 | |
|
28 | 23 26 27 | syl2anc | |
29 | 11 20 22 28 | mpbir3and | |
30 | id | |
|
31 | oveq1 | |
|
32 | 30 31 | oveq12d | |
33 | 32 | eleq2d | |
34 | 33 | rspcev | |
35 | 12 29 34 | syl2anc | |
36 | 10 35 | impbii | |
37 | 2 36 | bitri | |
38 | 37 | eqriv | |
39 | retop | |
|
40 | 1 39 | eqeltri | |
41 | iooretop | |
|
42 | 41 1 | eleqtrri | |
43 | 42 | rgenw | |
44 | iunopn | |
|
45 | 40 43 44 | mp2an | |
46 | 38 45 | eqeltrri | |
47 | zssre | |
|
48 | uniretop | |
|
49 | 1 | unieqi | |
50 | 48 49 | eqtr4i | |
51 | 50 | iscld2 | |
52 | 40 47 51 | mp2an | |
53 | 46 52 | mpbir | |