$\mathbb{R}\mathrm{/}\mathbb{Z}$ is compact and path-connected

Given: The quotient projection $p:\mathbb{R}\to \mathbb{R}\mathrm{/}\mathbb{Z}$.

For every real $x$ there is exactly one integer $m$ with $m\le x<m+1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m\le x<m+1$).

A subset $K\subseteq \mathbb{R}$ is compact for the usual metric if and only if it is closed and bounded (Heine-Borel in ${\mathbb{R}}^n$: with the Euclidean metric a subset of ${\mathbb{R}}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

If $f:X\to Y$ is continuous and $K\subseteq X$ is compact, then $f[K]$ is a compact subset of $Y$ (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

A space $X$ is path-connected when for every $x,y\in X$ there is a continuous path $\gamma :[0,1]\to X$ with $\gamma (0)=x$ and $\gamma (1)=y$ (Paths, path-connected spaces and path components).

The circle is $S^1:=\mathbb{R}\mathrm{/}\mathbb{Z}$ with the quotient topology induced by $p(x)=[x]$ and basepoint $[0]$; moreover $p^{-1}([0])=\mathbb{Z}$ and $p(x+n)=p(x)$ for every real $x$ and integer $n$ (The circle as $S^1=\mathbb{R}\mathrm{/}\mathbb{Z}$ with basepoint $[0]$).

For a metric space, metric compactness is equivalent to compactness in its metric topology, both for the whole space and for every subspace (For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide).

Every constant real-valued function and the identity are continuous, and finite sums, products, and scalar multiples of continuous functions are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

A composite of continuous maps is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).