Proof of A Real Hilbert Space with an Orthonormal Basis is Separable

Each result cited is universally quantified over the data in its own statement. For $n\in\mathbb{N}$ let $[n]$ be the initial segment determined by $n$, let $e^{(n)}$ be the $n$-tuple with components $e_{1},\dots,e_{n}$, and let $D_{n}$ be the set of those $z\in H$ for which there is $q\in\mathbb{Q}^{n}$ with $z=\sum_{k=1}^{n}q_{k}e_{k}$, so that $D$ is the union of the sets $D_{n}$ over $n\in\mathbb{N}$. The tuple $e^{(n)}$ is orthonormal, since its components are components of the orthonormal sequence $(e_{k})_{k\in\mathbb{N}}$ and distinct indices in $[n]$ are distinct in $\mathbb{N}$.

Claim 1, countability. Fix $n\in\mathbb{N}$. By claim 3 of The Integers and the Rational Numbers are Countable the set $\mathbb{Q}^{n}$ is countable, and $D_{n}$ is the set of values of the map $\mathbb{Q}^{n}\to H$ sending $q$ to $\sum_{k=1}^{n}q_{k}e_{k}$, so $D_{n}$ is countable by claim 4 of Basic Properties of Countable Sets. Hence $D$, the union of the countable sets $D_{n}$ over $n\in\mathbb{N}$, is countable by A Countable Union of Countable Sets is Countable.

Claim 1, density. Let $x\in H$ and let $\varepsilon$ be a positive real number, and put $c_{k}=\langle x,e_{k}\rangle$ for $k\in\mathbb{N}$. By Orthonormal Expansions in a Real Hilbert Space §expansion the series $\sum_{k=1}^{\infty}c_{k}e_{k}$ converges in $H$ with sum $x$, so there is $n\in\mathbb{N}$ such that the point $w=\sum_{k=1}^{n}c_{k}e_{k}$ satisfies $|x-w|<\tfrac{\varepsilon}{2}$.

For $k\in[n]$ the real number $\bigl(\tfrac{1}{2}\bigr)^{k}\tfrac{\varepsilon^{2}}{4}$ is positive, so by Existence and Uniqueness of the Nonnegative Square Root there is a nonnegative real $\eta_{k}$ with $\eta_{k}^{2}=\bigl(\tfrac{1}{2}\bigr)^{k}\tfrac{\varepsilon^{2}}{4}$; and $\eta_{k}$ is positive, since $\eta_{k}=0$ would give $\eta_{k}^{2}=0$ by claim 4 of Properties of Natural Number Powers in a Field, contrary to the positivity of that number. By claim 2 of The Rational Numbers are Dense in the Real Numbers the set of rational $q$ with $|c_{k}-q|<\eta_{k}$ is nonempty for each $k\in[n]$, so, these being finitely many nonempty sets, there is $q\in\mathbb{Q}^{n}$ with $|c_{k}-q_{k}|<\eta_{k}$ for every $k\in[n]$. Put $v=\sum_{k=1}^{n}q_{k}e_{k}$, a point of $D_{n}$ and hence of $D$.

For $k\in[n]$, claim 1 of Properties of the Absolute Value in an Ordered Field gives $|c_{k}-q_{k}|\in\{c_{k}-q_{k},q_{k}-c_{k}\}$ and $0\le|c_{k}-q_{k}|$, so in either case $|c_{k}-q_{k}|^{2}=(c_{k}-q_{k})^{2}$; by claim 1 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field applied to $0\le|c_{k}-q_{k}|<\eta_{k}$,

Write $\beta_{k}=\bigl(\tfrac{1}{2}\bigr)^{k}\tfrac{\varepsilon^{2}}{4}-(c_{k}-q_{k})^{2}$, which is nonnegative for $k\in[n]$ by the last display. By claim 2 of Properties of Finite Sums,

and the second sum on the right is nonnegative by claim 5 of that lemma, so claim 3 of Elementary Arithmetic in an Ordered Field gives

the last step by claim 3 of Properties of Finite Sums. The terms $\bigl(\tfrac{1}{2}\bigr)^{k}$ are nonnegative and, by Series of Nonnegative Real Numbers, Comparison, and the Geometric Series §geometric with $r=\tfrac{1}{2}$, the series $\sum_{k=1}^{\infty}\bigl(\tfrac{1}{2}\bigr)^{k}$ converges with sum $1$; so Series of Nonnegative Real Numbers, Comparison, and the Geometric Series §dominates gives $\sum_{k=1}^{n}\bigl(\tfrac{1}{2}\bigr)^{k}\le1$, and multiplying by the nonnegative number $\tfrac{\varepsilon^{2}}{4}$ with claim 5 of Elementary Arithmetic in an Ordered Field,

Now, by claim 2 of Properties of Finite Sums of Vectors applied to the maps $k\mapsto(c_{k}-q_{k})e_{k}$ and $k\mapsto q_{k}e_{k}$ on $[n]$, together with the distributive law of the vector space $H$,

so $w-v=\sum_{k=1}^{n}(c_{k}-q_{k})e_{k}$, and Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §norm, applied to the orthonormal tuple $e^{(n)}$ and the coefficients $c_{k}-q_{k}$, gives

Both $|w-v|$ and $\tfrac{\varepsilon}{2}$ are nonnegative, so $|w-v|\le\tfrac{\varepsilon}{2}$: otherwise $\tfrac{\varepsilon}{2}<|w-v|$ and claim 1 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field would give $\bigl(\tfrac{\varepsilon}{2}\bigr)^{2}<|w-v|^{2}$, contradicting the last display by trichotomy.

Since $d$ is a metric by The Norm Metric of a Real Inner Product Space: Triangle Inequalities, Limits and Continuity §metric and $d(y,z)=|y-z|$ for $y,z\in H$, the triangle inequality and claim 3 of Elementary Order Arithmetic in an Ordered Field give

Thus every open ball about $x$ meets $D$, so $x$ lies in the closure of $D$ by Characterization of the Closure in a Metric Space by Open Balls. As $x\in H$ was arbitrary, the closure of $D$ is $H$, that is, $D$ is dense in $H$.

Claim 2. By claim 1 the set $D$ is a countable dense subset of $H$, which is exactly the condition for $(H,d)$ to be separable in the sense of Separable Metric Space.