[proofplan] We extract a countable subset of the unit sphere of $X^*$, use [Hahn-Banach (Normed Space Version)](/theorems/2629) to attach a vector $x_n \in X$ at which each $f_n$ is "almost norming", and prove that the rational-linear span of $(x_n)$ is dense in $X$. The argument proceeds by contradiction: if the closed span $W$ of these vectors is not all of $X$, the [Hahn-Banach (Normed Space Version)](/theorems/2629) produces a non-zero functional vanishing on $W$, contradicting density of $(f_n)$ on the unit sphere of $X^*$. [/proofplan] [step:Choose a countable dense set in the unit sphere of $X^*$] Since $X^*$ is separable, it contains a countable dense subset $\{g_n : n \in \mathbb{N}\}$. We may assume each $g_n \ne 0$ by removing the zero functional if it appears (a single removal preserves density). Define \begin{align*} f_n := \frac{g_n}{\|g_n\|_{X^*}} \in X^*, \qquad n \in \mathbb{N}, \end{align*} so $\|f_n\|_{X^*} = 1$ for every $n$. The sequence $(f_n)$ is dense in the unit sphere $S_{X^*} = \{f \in X^* : \|f\|_{X^*} = 1\}$. Indeed, given $f \in S_{X^*}$ and $\varepsilon \in (0, 1)$, density of $(g_n)$ provides $n$ with $\|g_n - f\|_{X^*} < \varepsilon/2$. Then by the reverse triangle inequality $|\|g_n\|_{X^*} - 1| < \varepsilon/2$, so \begin{align*} \|f_n - f\|_{X^*} \le \|f_n - g_n\|_{X^*} + \|g_n - f\|_{X^*} = |1 - \|g_n\|_{X^*}| + \|g_n - f\|_{X^*} < \varepsilon. \end{align*} [guided] Why normalise to the unit sphere rather than work with the original sequence $(g_n)$? Because the next step picks an "almost-norming" vector for each functional: a vector $x_n$ with $|f_n(x_n)| \ge 1/2$ when $\|f_n\| = 1$. Normalising upfront makes the threshold $1/2$ uniform; with the unnormalised $g_n$ we would have to track variable thresholds $\|g_n\|/2$ that could collapse to zero. The reverse triangle inequality $|\|g_n\| - \|f\|| \le \|g_n - f\|$ is what controls the normalisation cost: if $g_n$ is close to a unit-norm $f$, then $\|g_n\|$ is close to $1$, so dividing by $\|g_n\|$ does not move $g_n$ far. The estimate $\|f_n - g_n\| = |1 - \|g_n\||$ comes from $f_n - g_n = (1/\|g_n\| - 1)g_n$, whose norm equals $|1 - \|g_n\||$. [/guided] [/step] [step:Pick almost-norming vectors $x_n \in S_X$ for each $f_n$] For each $n$, the operator norm $\|f_n\|_{X^*} = \sup_{\|x\|_X \le 1} |f_n(x)| = 1$. By definition of supremum, there exists $x_n \in X$ with $\|x_n\|_X \le 1$ and \begin{align*} |f_n(x_n)| \ge \tfrac{1}{2}. \end{align*} [guided] The constant $1/2$ is not load-bearing: any threshold $\theta \in (0, 1)$ would work. We use $1/2$ for concreteness, as is standard in this argument. The point of the inequality $|f_n(x_n)| \ge \theta\|f_n\|$ is that we are passing from a norm defined as a supremum over the (uncountable) unit ball to a witness that nearly attains the supremum. Since $\|f_n\|_{X^*} = 1$, there exist vectors in the unit ball where $|f_n|$ is arbitrarily close to $1$; we pick any one with $|f_n(x_n)| \ge 1/2$. [/guided] [/step] [step:Define the candidate dense subspace and reduce to showing $W = X$] Let \begin{align*} W := \overline{\operatorname{span}_{\mathbb{Q}}\{x_n : n \in \mathbb{N}\}} \subseteq X, \end{align*} the closure of the $\mathbb{Q}$-linear span of $(x_n)$ in the norm of $X$ (in the complex case, replace $\mathbb{Q}$ by $\mathbb{Q} + i\mathbb{Q}$). The set $\operatorname{span}_{\mathbb{Q}}\{x_n\}$ is countable as a countable union (over the finite supports) of countable sets (finite $\mathbb{Q}$-linear combinations on a countable index set). We claim $W = X$. Granting this claim, $X$ is the closure of a countable set, hence separable. The remainder of the proof establishes $W = X$ by contradiction. [/step] [step:Suppose $W \ne X$ and produce a separating functional via Hahn-Banach] Suppose for contradiction that $W \subsetneq X$. Note that $W$ is a closed subspace of $X$ (it is a closed set, and it is a subspace because the closure of a $\mathbb{Q}$-linear subspace in a normed space over $\mathbb{R}$ or $\mathbb{C}$ is a $\mathbb{R}$- or $\mathbb{C}$-linear subspace: scalar multiples and sums lie in the closure by continuity of vector operations and density of $\mathbb{Q}$ in $\mathbb{R}$). Pick $x_0 \in X \setminus W$. Since $W$ is closed, $\operatorname{dist}(x_0, W) > 0$. By the [Hahn-Banach (Normed Space Version)](/theorems/2629) applied to the closed subspace $W \subseteq X$ and the point $x_0 \in X \setminus W$ (the standard separating-functional consequence of Hahn-Banach), there exists $f \in X^*$ with \begin{align*} \|f\|_{X^*} = 1, \qquad f|_W = 0, \qquad f(x_0) = \operatorname{dist}(x_0, W) > 0. \end{align*} In particular, $f(x_n) = 0$ for every $n$, since each $x_n \in W$. [guided] The standard form of the [Hahn-Banach (Normed Space Version)](/theorems/2629) used here is the **separation of a point from a closed subspace**: given a closed subspace $W \subset X$ and $x_0 \notin W$, there is $f \in X^*$ with $\|f\| = 1$, $f|_W = 0$, and $f(x_0) = \operatorname{dist}(x_0, W)$. Why is this consequence equivalent to the support-functional version? Pass to the quotient $X/W$ (well-defined because $W$ is closed, by the [Quotient Norm and the Quotient Map](/theorems/2631)). The element $x_0 + W \in X/W$ has norm $\operatorname{dist}(x_0, W) > 0$. Apply the support-functional consequence of the [Hahn-Banach (Normed Space Version)](/theorems/2629) on $X/W$ to get $\tilde f \in (X/W)^*$ with $\|\tilde f\| = 1$ and $\tilde f(x_0 + W) = \|x_0 + W\| = \operatorname{dist}(x_0, W)$. Composing with the quotient map gives $f := \tilde f \circ q \in X^*$ with $\|f\| = 1$ (since $q$ is a quotient map of norm $1$ that opens onto unit balls), $f|_W = 0$, and $f(x_0) = \operatorname{dist}(x_0, W)$. The key feature: this $f$ is non-zero ($f(x_0) > 0$), has unit norm, and annihilates every $x_n$. [/guided] [/step] [step:Derive a contradiction using density of $(f_n)$ on $S_{X^*}$] The functional $f \in S_{X^*}$ from the previous step has $f(x_n) = 0$ for all $n$. By the density established above, there exists $n$ with \begin{align*} \|f_n - f\|_{X^*} < \tfrac{1}{2}. \end{align*} Evaluating both sides of the inequality $|(f_n - f)(x_n)| \le \|f_n - f\|_{X^*} \|x_n\|_X$ and using $\|x_n\|_X \le 1$ together with $f(x_n) = 0$: \begin{align*} |f_n(x_n)| = |f_n(x_n) - f(x_n)| = |(f_n - f)(x_n)| \le \|f_n - f\|_{X^*} \|x_n\|_X < \tfrac{1}{2}. \end{align*} This contradicts the choice $|f_n(x_n)| \ge 1/2$ from the second step. Hence the supposition $W \ne X$ is false, so $W = X$. [guided] The whole argument compresses to a single tension. On one hand, by construction, $f_n$ is "almost as large as it can be" at $x_n$: $|f_n(x_n)| \ge 1/2$. On the other hand, if $W$ misses some point of $X$, then by the [Hahn-Banach (Normed Space Version)](/theorems/2629) we can manufacture a unit-norm functional $f$ that **annihilates every $x_n$**. Density of $(f_n)$ in the unit sphere $S_{X^*}$ forces some $f_n$ within $1/2$ of $f$, so by linearity $|f_n(x_n)|$ is within $1/2$ of $|f(x_n)| = 0$, i.e. less than $1/2$. The two bounds collide. Note where each separability ingredient enters: - **Density of $(f_n)$ in $S_{X^*}$** (from $X^*$ separable) is used to find $f_n$ near the manufactured $f$. - **Hahn-Banach** is used to manufacture $f$. - **Almost-norming choice** of $x_n$ is the bookkeeping that turns the closeness $\|f_n - f\| < 1/2$ into the impossible inequality $1/2 \le |f_n(x_n)| < 1/2$. If we had only assumed $X^*$ has a countable dense subset of the unit ball (rather than the unit sphere), the same proof works after the renormalisation step. [/guided] [/step] [step:Conclude separability of $X$] By the previous step, $X = W$, where $W$ is the closure of the countable set $\operatorname{span}_{\mathbb{Q}}\{x_n : n \in \mathbb{N}\}$ in $X$. A normed space that is the closure of a countable set is separable. Hence $X$ is separable. [/step]