It is well-known that the set of nonnegative integers $\mathbb{N}$ is [definable][1] in the ring of integers $\mathbb{Z}$. Indeed, by [Lagrange's four squares theorem][2] 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.


  [1]: https://en.wikipedia.org/wiki/Definable_set
  [2]: https://en.wikipedia.org/wiki/Lagrange%27s_four-square_theorem