A nonzero polynomial over a field is separable exactly when its gcd with its derivative is $1$

If $\gcd (f,f^{\mathrm{\prime }})=1$, [L2] says that the gcd remains $1$ in every extension field, and [L7] supplies a Bézout identity there. A common root of $f$ and $f^{\mathrm{\prime }}$ would evaluate that identity to $0=1$ by [L5], so [L1] shows that $f$ has no repeated root and is separable.

Conversely, if $d=\gcd (f,f^{\mathrm{\prime }})\mathrm{\ne }1$, then $d$ is a nonconstant nonunit and [L4] supplies an irreducible factor $p$ of $d$. Fact [L3] makes $E=F[x]\mathrm{/}(p)$ a field. No nonzero constant lies in $(p)$ because a nonconstant polynomial cannot divide it, so [L6] makes the canonical map $F\to E$ injective and identifies $F$ with a subfield of $E$. Under the evaluation map of [L5], the residue class of $x$ is a common root in $E$ of $p$, hence of $d$, $f$, and $f^{\mathrm{\prime }}$.

By [L1], the common root from step 1.2 is a repeated root of $f$, so a separable $f$ must have $d=1$; combined with step 1.1, this proves the biconditional.