Sylow existence by subset action (source code)

= Sylow existence by subset action
{c}

Let $|G|=p^nr$ with $p\nmid r$. The coefficient of $X^{p^n}$ in $(1+X)^{p^nr}$ is $r$ modulo $p$, because $(1+X)^{p^nr}=(1+X^{p^n})^r$ over the field of $p$ elements. Thus the number of subsets of size $p^n$ is not divisible by $p$. Left translation of $G$ on those subsets has an orbit of index prime to $p$. Its stabilizer acts freely on its subset, so its order divides $p^n$, while its prime-to-$p$ index forces its order to be $p^n$. This proves existence of a <Sylow subgroup> without an induction using Cauchy's theorem.