Proof of Triangular Numbers

Throughout, claim numbers for the canonical map $\iota$ refer to Properties of the Canonical Map from the Natural Numbers to an Ordered Field, order manipulations in $\mathbb{R}$ use Elementary Order Arithmetic in an Ordered Field, and claim numbers for the order on $\mathbb{N}$ refer to Properties of the Order on the Natural Numbers.

Claim 1. Let $E$ be the set of those $k\in\mathbb{N}$ for which there exists $n\in\mathbb{N}$ with $2\,\iota(n)=\iota(k)\bigl(\iota(k)+1\bigr)$.

$1\in E$. By claim 1, $\iota(1)=1$, so $\iota(1)\bigl(\iota(1)+1\bigr)=1\cdot 2=2=2\,\iota(1)$, and $n=1$ has the required property.

$k\in E$ implies $k+1\in E$. Let $n\in\mathbb{N}$ satisfy $2\,\iota(n)=\iota(k)\bigl(\iota(k)+1\bigr)$. By claim 1, $\iota(k+1)=\iota(k)+1$, so the field operations of $\mathbb{R}$ give

By claim 4 (additivity), $\iota(n)+\iota(k+1)=\iota\bigl(n+k+1\bigr)$, so the right-hand side equals $2\,\iota(n+k+1)$ and $k+1\in E$.

By Principle of Induction for the Natural Numbers, $E=\mathbb{N}$.

Uniqueness. In $\mathbb{R}$ one has $0<1$ by claim 6 of Elementary Order Arithmetic in an Ordered Field and $0<2$ by claim 8 of that lemma, so $2\ne0$ and $2$ is invertible. If $2\,\iota(n)=2\,\iota(n')$ then $\iota(n)=\iota(n')$, hence $n=n'$ by claim 7 (injectivity). Writing $T_{k}$ for the unique natural number attached to $k$ in this way defines a family $(T_{k})_{k\in\mathbb{N}}$ with all terms in $\mathbb{N}$, that is, a sequence in $\mathbb{N}$.

Claim 2. The base case above exhibits $n=1$ with $2\,\iota(1)=\iota(1)(\iota(1)+1)$, so $T_{1}=1$ by uniqueness. The induction step, applied with $n=T_{k}$, exhibits $n+k+1=T_{k}+k+1$ as a natural number whose image satisfies the defining equation for $k+1$, so $T_{k+1}=T_{k}+k+1$, again by uniqueness.

Claim 3. First let $k\in\mathbb{N}$ be arbitrary. By claim 2 and claim 4 (additivity),

and $0<\iota(k+1)$ by claim 3 (positivity), so $\iota(T_{k})<\iota(T_{k+1})$. By trichotomy (claim 3 of the order lemma) exactly one of $T_{k+1}<T_{k}$, $T_{k+1}=T_{k}$, $T_{k}<T_{k+1}$ holds; the first would give $\iota(T_{k+1})<\iota(T_{k})$ by claim 6 (strict monotonicity) and the second $\iota(T_{k+1})=\iota(T_{k})$, both contradicting $\iota(T_{k})<\iota(T_{k+1})$. Hence $T_{k}<T_{k+1}$.

Now fix $k\in\mathbb{N}$ and let $l\in\mathbb{N}$ with $k<l$. By claim 7 of the order lemma there is $j\in\mathbb{N}$ with $l=k+j$, so it suffices to prove, by induction on $j$, that $T_{k}<T_{k+j}$ for every $j\in\mathbb{N}$. For $j=1$ this is the previous paragraph. If $T_{k}<T_{k+j}$, then $T_{k+j}<T_{k+j+1}=T_{k+(j+1)}$ by the previous paragraph and associativity of addition (claim 3 of Arithmetic of Addition on the Natural Numbers), so $T_{k}<T_{k+(j+1)}$ by transitivity (claim 1 of the order lemma). By Principle of Induction for the Natural Numbers the assertion holds for every $j$, which proves claim 3.