Every principal ideal domain is a unique factorisation domain

Suppose, for contradiction, that some nonzero nonunit is not a product of irreducibles. The principal ideals generated by such bad elements form a nonempty family; by [L1] and [L2], choose a maximal member $(a)$. This use of the maximal condition spends DC, supplied by the assumed AC. The element $a$ is not irreducible, so $a=bc$ with nonunit nonzero $b,c$. Then $(a)$ is strictly contained in both $(b)$ and $(c)$: for example, $(a)=(b)$ would give $b=at=bct$ and cancellation would make $c$ a unit. Maximality therefore makes $b$ and $c$ products of irreducibles, and their product is a factorization of $a$, a contradiction. Thus every nonzero nonunit factors into irreducibles.

For uniqueness, if $p_1\cdots p_r=q_1\cdots q_s$ are irreducible factorizations, primality of $p_1$ from [L3] makes it divide some $q_j$, hence the two factors are associates. Cancel them in the domain and repeat on the remaining finite product. This induction pairs every factor and shows $r=s$ up to order and associates; the empty product is the unit case.

Step 1.1 gives factorization existence and step 1.2 gives the uniqueness required in the UFD definition. Therefore every PID is a UFD; the contradictory assumption in step 1.1 is discharged.