A detailed proof can be found in Neerven's Functional Analysis, which the author generously distributes online for free. In the v5 edition this is proposition $4.46$. The proof is quite detailed, and the only implication that might block the new learners is why $x_0^{\ast\ast}$ is continuous wrt the weak $\ast $ topology. In fact, more generally we have the following statement:
A functional on $X^{\ast}$, $\varphi:X^{\ast}\to\mathbb{C}$ is bounded
on $U\subseteq X^{\ast}$ a weak-$\ast$ open set $\implies$ $\varphi$
is continuous wrt the weak-$\ast$ topology (and the usual topology on
$\mathbb{C}$).
Proof: $U$ contains a basis open set
$$\tilde{U}= \{f\in X^{\ast}\ |\ |(f-g)(x_j)|<\epsilon_0\text{ for } 1\le j\le n\} $$
for some fixed $\epsilon_0>0$, $x_1,\cdots,x_n\in X$ and $g\in X^{\ast}$. Since $\varphi$ is bounded on $U$, it is a fortiori bounded on $\tilde{U}$. Suppose $f\in \tilde{U}\implies|\varphi(f)|<M$. Then $|\varphi(f-g)|<M+|\varphi(g)|$ for all $f\in \tilde{U}$. That is $\varphi$ is also bounded on
$$ \hat{U}= \{f\in X^{\ast}\ |\ |f(x_j)|<\epsilon_0\text{ for } 1\le j\le n\} . $$
For we do not need the old $U$ and $\tilde{U}$ from now on, we may now re-denote
$$ U=\{f\in X^{\ast}\ |\ |f(x_j)|<\epsilon_0\text{ for } 1\le j\le n\} $$
and $\varphi$ is still bounded on $U$. Suppose $|\varphi(f)|<M$ for all $f\in U$.
For all $\epsilon>0$ fixed, if
$$f\in O:=\{h\in X^{\ast}\ |\ |h(x_j)|<\frac{\epsilon_0\epsilon}{M}\text{ for } 1\le j\le n\},$$
then $\frac{M}{\epsilon}f\in U$ $\implies$ $M>|\varphi(\frac{M}{\epsilon}f)|=\frac{M}{\epsilon}|\varphi(f)|$, i.e.
$|\varphi(f)|<\epsilon$.
That is, for all open set $\mathcal{O}$ in $\mathbb{C}$ containing $0$, exists a basis element $O$ of the weak-$\ast$ topology containing $0 (\text{ of } X^{\ast})$, s.t. $\varphi(O)\subseteq\mathcal{O}$, i.e. $\varphi$ is continuous wrt weak-$\ast$ topology at $0_{X^{\ast}}$.
Finally we show the continuity at general points by a translation. For arbitrary $f_0\in X^{\ast}$ fixed, use $f-f_0$ to substitute $f$ in the above paragraph, and also note that
$\varphi(f-f_0)=\varphi(f)-\varphi(f_0)$ since
$\varphi$ is linear. This shows for arbitrary $f_0\in X^{\ast}$, $\varphi$ is continuous wrt weak-$\ast$ topology. $\square$