Suppose we have a time-homogeneous, discrete-time, aperiodic, positive recurrent, irreducible Markov chain $(X_t)_{t \geq 0}$ on a discrete state space $E$. It is known that its stationary distribution is given by $$\pi(x)=\frac{1}{E_x[H_x]}, \quad x \in E,$$ where $H_x$ is the first positive time of visiting $x$ when starting at $x$, i.e.
$$H_x:=\inf\{t \geq 1 \colon X_t= x\}.$$
Why do we know that it is a distribution, so how can one formally see that
$$\sum_{x \in E} \frac{1}{E_x[H_x]}=1?$$
I know about the intuition, but I would really like to see a very formal proof of it or at least a hint how to prove it very formally.