A symmetric operator on a separable Hilbert space has a real non-eigenvalue

Let $E$ be a separable real inner product space and let $A$ be a linear operator defined on a subspace $D(A)\subseteq E$ (a partially defined linear map $E\to E$). Suppose $A$ is symmetric: $\langle Ax,y\rangle=\langle x,Ay\rangle$ for all $x,y\in D(A)$. Then there is a real number $\mu$ that is not an eigenvalue of $A$: if $f\in D(A)$ and $Af=\mu f$, then $f=0$.

Role: this supplies a real point $\mu$ with $\ker(A-\mu)=0$, needed to speak of the resolvent $(A-\mu)^{-1}$ of a symmetric differential operator (for example the asymptotic operator $A_S=-J_0\partial_t-S$ on $L^2(S^1,\mathbb R^{2n})$) without leaving the real numbers.

Formalization note: E →ₗ.[ℝ] E is Mathlib's LinearPMap (a linear map on the submodule A.domain), and A.IsFormalAdjoint A is Mathlib's symmetry condition ⟪A x, y⟫ = ⟪x, A y⟫ for x y : A.domain. Separability is the typeclass TopologicalSpace.SeparableSpace E; completeness is not assumed.