It is well-known that the set of nonnegative integers $\mathbb{N}$ is definable in the ring of integers $\mathbb{Z}$. Indeed, by Lagrange's four squares theorem we have $\mathbb{N} = \{n \in \mathbb{Z} : \varphi(n)\}$, where $\varphi$ is the formula
$$\varphi(x) := \exists a\, \exists b\, \exists c\, \exists d \; x = a^2 + b^2 + c^2 + d^2$$
However, Lagrange's theorem is not so trivial, so I wonder:
Is there a more elementary and self-contained proof of the definability of $\mathbb{N}$ in the ring of integers?
Thank you.