The Laurent polynomial ring is Noetherian and a unique factorisation domain

Noetherian. Every nonzero ideal of $\mathbb{Z}$ is generated by its least positive element, by integer division, and the zero ideal is generated by $0$; thus $\mathbb{Z}$ is Noetherian. By [F2] the polynomial ring $\mathbb{Z}[t]$ is Noetherian, and $\mathrm{\Lambda }=\mathbb{Z}[t{]}_S$ is a localisation of it; localisations of Noetherian rings are Noetherian by [F2]. Hence every ideal of $\mathrm{\Lambda }$ is finitely generated. In $\mathbb{Z}[t]$, if $t$ divides $fg$, evaluation at zero gives $f(0)g(0)=0$ in the domain $\mathbb{Z}$, so one constant term vanishes and $t$ divides that factor. Since $t$ is nonzero and a nonunit there, it is prime; localization then makes it a unit by [F1].

The integer-polynomial UFD. Write any nonzero integer polynomial as its integer content times a primitive polynomial. Factor the latter over $\mathbb{Q}[t]$ by [F3], and clear denominators and contents in each nonconstant factor to obtain primitive integer factors. Their product is primitive by Gauss' lemma. Two primitive integer polynomials related by a nonzero rational scalar differ only by sign: a reduced denominator would divide every coefficient of the first, and the scalar's numerator would divide every coefficient of the second. Hence the primitive polynomial is, up to sign, the product of these primitive factors, which are irreducible over $\mathbb{Z}$ by Gauss' lemma. Integer prime factors of the content complete the factorization. Uniqueness follows by comparing integer contents using integer factorization, then comparing the remaining factors in the UFD $\mathbb{Q}[t]$; primitive rational associates are integer associates by the same scalar argument. Thus $\mathbb{Z}[t]$ is a UFD, and its irreducibles are prime.

Surviving irreducibles. An irreducible $p\in \mathbb{Z}[t]$ becomes a unit in $\mathrm{\Lambda }$ exactly when it divides a power of $t$: a relation $(p\mathrm{/}1)(a\mathrm{/}{t}^N)=1$ is equivalent, by injectivity of the localisation map, to $pa=t^N$, and the converse gives an inverse. Suppose $p$ remains a nonunit and $p=xy$ in $\mathrm{\Lambda }$. Write $x=a\mathrm{/}{t}^N$ and $y=b\mathrm{/}{t}^M$. Then $p{t}^{N+M}=ab$ in $\mathbb{Z}[t]$. The UFD property of step 1.2 makes $p$ prime, so, after interchanging $x,y$, write $a=p{a}^{\mathrm{\prime }}$. Cancellation gives $a^{\mathrm{\prime }}b=t^{N+M}$, hence $y(a^{\mathrm{\prime }}\mathrm{/}{t}^N)=1$. Thus $p$ is irreducible in $\mathrm{\Lambda }$.

Existence and uniqueness. Every nonzero nonunit $x\in \mathrm{\Lambda }$ has the form $a\mathrm{/}{t}^N$ with $0\mathrm{\ne }a\in \mathbb{Z}[t]$. Factor $a$ using step 1.2 and absorb all factors associated to $t$ into a Laurent unit. Step 2.1 shows that all remaining factors are irreducible in $\mathrm{\Lambda }$, giving existence. In particular every irreducible of $\mathrm{\Lambda }$ is associate there to one of these surviving integer-polynomial primes: its factorization can contain only one nonunit factor. To compare two Laurent factorizations, replace their factors by these integer-polynomial primes and absorb their Laurent units, which are $\pm t^k$ by [F1]. Clearing powers of $t$ gives equality in $\mathbb{Z}[t]$. Uniqueness there matches all primes not associated to $t$ on the two sides, hence matches the original Laurent factors up to permutation and Laurent units. Together with step 1.1, this proves the statement.