Initial Segment of One-Based Natural Numbers determined by Zero is Empty

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\N^*_k$ denote the initial segment of the one-based natural numbers determined by $k$:

$\N^*_k = \set {1, 2, 3, \ldots, k - 1, k}$


Then $\N^*_0 = \O$.


Proof

From the definition of $\N^*_0$:

$\N^*_0 = \set {n \in \N_{>0}: n \le 0}$

From the definition of one, the minimal element of $\N_{>0}$ is $1$.

From Zero Strictly Precedes One we know that $0 < 1$.

So there is no element $n$ of $\N_{>0}$ such that $n \le 0$.

Thus $\N^*_0 = \O$.

$\blacksquare$


Also see