Description: The integers are a closed set in the topology on CC . (Contributed by Mario Carneiro, 17-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | recld2.1 | ⊢ 𝐽 = ( TopOpen ‘ ℂfld ) | |
| Assertion | zcld2 | ⊢ ℤ ∈ ( Clsd ‘ 𝐽 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | recld2.1 | ⊢ 𝐽 = ( TopOpen ‘ ℂfld ) | |
| 2 | 1 | recld2 | ⊢ ℝ ∈ ( Clsd ‘ 𝐽 ) |
| 3 | 1 | tgioo2 | ⊢ ( topGen ‘ ran (,) ) = ( 𝐽 ↾t ℝ ) |
| 4 | 3 | eqcomi | ⊢ ( 𝐽 ↾t ℝ ) = ( topGen ‘ ran (,) ) |
| 5 | 4 | zcld | ⊢ ℤ ∈ ( Clsd ‘ ( 𝐽 ↾t ℝ ) ) |
| 6 | restcldr | ⊢ ( ( ℝ ∈ ( Clsd ‘ 𝐽 ) ∧ ℤ ∈ ( Clsd ‘ ( 𝐽 ↾t ℝ ) ) ) → ℤ ∈ ( Clsd ‘ 𝐽 ) ) | |
| 7 | 2 5 6 | mp2an | ⊢ ℤ ∈ ( Clsd ‘ 𝐽 ) |