Nonzero natural number has successor

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\N$ be the 0-based natural numbers:

$\N = \left\{{0, 1, 2, \ldots}\right\}$

Let $s: \N \to \N: \map s n = n + 1$ be the successor function.

Then:

$\forall n \in \N \setminus \set 0 \left( \exists m \in \N: \map s m = n\right)$