Irreducible elements of a principal ideal domain are prime (source code)

= Irreducible elements of a principal ideal domain are prime

Let $\pi$ be an <irreducible element> of a <principal ideal domain> $R$, and suppose $\pi\nmid a$. The <ideal> $(\pi,a)=(d)$ has generator $d$ dividing $\pi$. Irreducibility makes $d$ a <unit> or an associate of $\pi$; the latter would imply $\pi\mid a$. Hence $(\pi,a)=R$, giving $u\pi+va=1$ for some $u,v\in R$. If $\pi\mid ab$, multiply this identity by $b$: both $u\pi b$ and $vab$ are divisible by $\pi$, so $\pi\mid b$. This is precisely the <prime element> property.