How to prove that for all $z \in \mathbb{Z}$ with $z > 0$ there is an $n \in \mathbb{N}$ with $n > 0$ such that $z = \underbrace{1 + 1 + \dots + 1}_{n \text{ times}}$, or as a logical formula:
$$(\forall z \in \mathbb{Z})\ z > 0 \rightarrow \big(\ (\exists n \in \mathbb{N})\ n > 0 \ \wedge\ z = \underbrace{1 + 1 + \dots + 1}_{n \text{ times}}\ \big)$$
or respectively
$$(\forall z \in \mathbb{Z})\ z > 0 \rightarrow \big(\ (\exists n \in \mathbb{N})\ n > 0 \ \wedge\ z = n \times 1\ \big)$$
with $z = n \times 1 :\equiv \underbrace{1 + 1 + \dots + 1}_{n \text{ times}}$
Note that this is a "second-order" statement because $n$ is not taken from the realm of $\mathbb{Z}$, and the expression $\underbrace{1 + 1 + \dots + 1}_{n \text{ times}}$ is not a first-order expression, respectively $z = n \times 1$ is not an expression in the language of $\mathbb{Z}$. Note further that $0$ appears in two different meanings: Once as the neutral element of $(\mathbb{Z},+)$, the other time as the neutral element of $(\mathbb{N},+)$.
My question is, how to state and prove this statement rigorously, making use of which – possibly set-theoretical – notions and arguments?
I assume that $\mathbb{Z}^+$ is not defined beforehand as the set of sums $\{1, 1+1, 1+1+1, \dots\}$