Solution (source code)

= Solution

If the <prime> $p$ does not divide $x$, then $\gcd(p,x)=1$. The <Bezout identity> gives <integers> $a,b$ with $ap+bx=1$. Multiplying by $y$ gives $apy+bxy=y$. If $p\mid xy$, both terms on the left are divisible by $p$, so $p\mid y$. Thus <Euclid lemma> holds:
$$
\boxed{p\mid xy\implies p\mid x\text{ or }p\mid y.}
$$
For completeness, existence in the <Fundamental theorem of arithmetic> follows by strong induction on a positive <integer> $n>1$. If $n$ is <prime> there is nothing to prove; otherwise $n=ab$ with $1<a,b<n$, and the inductive <prime> factorizations of $a,b$ give one for $n$. The <integer> $1$ has the empty factorization.

For uniqueness, suppose $p_1\cdots p_r=q_1\cdots q_s$ are two <prime> factorizations. Repeated application of <Euclid lemma> shows that $p_1$ divides some $q_j$. Both are <primes>, so they are equal. Reorder the second list, cancel this equal factor, and repeat. All factors must be matched, including their multiplicities. Thus \b[<prime factorization> exists and is unique up to the order of its factors]. For nonzero negative <integers> one also records the sign.