Units, powers and the domain property of the Laurent polynomial ring

Normal form. Write a nonzero element of ${\mathrm{\Lambda }}_1$ as $p\mathrm{/}{t}^N$ with $p\in \mathbb{Z}[t]$, $N\ge 0$ by [F1], and factor out the largest power of $t$ dividing $p$: there are $d\ge 0$ and $q\in \mathbb{Z}[t]$ with $p=t^{d}q$ and $t\nmid q$, the latter meaning $q(0)\mathrm{\ne }0$. Then $p\mathrm{/}{t}^N=t^{d-N}q$, so every nonzero element has a representative $t^{m}q$ with $m\in \mathbb{Z}$ and $q(0)\mathrm{\ne }0$. This representative is unique: if $t^{m}q=t^{m^{\mathrm{\prime }}}{q}^{\mathrm{\prime }}$ with $q(0),q^{\mathrm{\prime }}(0)\mathrm{\ne }0$, multiply by $t^{-m}$ to get $q=t^{m^{\mathrm{\prime }}-m}{q}^{\mathrm{\prime }}$; if $m^{\mathrm{\prime }}\ge m$, the constant term of the right-hand side equals $q^{\mathrm{\prime }}(0)\mathrm{\ne }0$ when $m^{\mathrm{\prime }}=m$ and vanishes when $m^{\mathrm{\prime }}>m$, while the constant term of $q$ is $q(0)\mathrm{\ne }0$, so $m^{\mathrm{\prime }}=m$ and $q=q^{\mathrm{\prime }}$; the case $m^{\mathrm{\prime }}<m$ is symmetric.

${\mathrm{\Lambda }}_1$ is an integral domain. Suppose $uv=0$ with $u=t^{m}p$, $v=t^{n}q$ nonzero in normal form, so $p(0),q(0)\mathrm{\ne }0$ and $pq\mathrm{\ne }0$ by [F3]. Then $uv=t^{m+n}pq$. If $m+n\ge 0$, the element $t^{m+n}pq$ is a polynomial, and [F2] yields $k\ge 0$ with $t^k{t}^{m+n}pq=t^{k+m+n}pq=0$ in $\mathbb{Z}[t]$; since $t^{k+m+n}\mathrm{\ne }0$ and $\mathbb{Z}[t]$ is a domain by [F3], $pq=0$, a contradiction. If $m+n<0$, the element is $pq\mathrm{/}{t}^{-(m+n)}$, and [F2] yields $k\ge 0$ with $t^{k}pq=0$ in $\mathbb{Z}[t]$, again forcing $pq=0$ by [F3], a contradiction. Hence $uv\mathrm{\ne }0$, so ${\mathrm{\Lambda }}_1$ is a domain.

Distinct powers of $t$. The elements $t^m=t^m\cdot 1$ and $1=t^0\cdot 1$ are in normal form, since the constant polynomial $1$ has $1\mathrm{\ne }0$. By uniqueness in step 1.1, $t^m=1$ forces $m=0$ and $q=1$. More generally $t^m=t^{m^{\mathrm{\prime }}}$ forces $t^{m-m^{\mathrm{\prime }}}=1$, hence $m=m^{\mathrm{\prime }}$.

Units. If $u=\pm t^m$, then $u\cdot (\pm t^{-m})=1$, so $u$ is a unit. Conversely let $u=t^{m}p$ in normal form be a unit, with inverse $v=t^{n}q$ in normal form; then $t^{m+n}pq=1$. Applying the normal form uniqueness of step 1.1 to $t^{m+n}pq$ and to $1=t^0\cdot 1$ gives $m+n=0$ and $pq=1$ in $\mathbb{Z}[t]$. By [F4] the unit $p$ of $\mathbb{Z}[t]$ is one of the two constants $\pm 1$; hence $u=\pm t^m$.

The sum $1+t+\cdots +t^{n-1}$. For $n\ge 2$ put $f=1+t+\cdots +t^{n-1}$, a polynomial with constant term $1$ and at least two nonzero coefficients. In normal form $f=t^{0}f$. If $f$ were a unit, step 2.3 would give $f=\pm t^m$ for some $m$; two elements equal in ${\mathrm{\Lambda }}_1$ have the same normal-form exponent and polynomial by step 1.1, so $m=0$ and $f=\pm 1$, contradicting that $f$ has at least two nonzero coefficients. Hence $f$ is not a unit, which is (d); claims (a), (b), (c) are steps 2.1, 2.2 and 2.3. No choice principle is used.