Check proof of Fermat's Little Theorem

Question

I wrote an informal proof of Fermat's Little Theorem. Can someone check to see if the reasoning is valid, and if so how I could formalize it:

Theorem: $n^{p-1} \equiv 1 \pmod p$

1. $ n \times 2n \times 3n \times ... \times (p-1)n = (p-1)!n^{p-1}$

2. $n\pmod p \ne 2n \pmod p \ne ... (p-1)n \pmod p$

If equation 2 wasn't true, then for 2 different integers $a$ and $b$ within $0$ to $p-1$, $an \pmod p = bn \pmod p$, meaning $a = b$, a contradiction.

Since $n\pmod p, 2n \pmod p , ... (p-1)n \pmod p$ have all different values and none are zero, $n\pmod p, 2n \pmod p , ... (p-1)n$ has all values from $1$ to $p-1$.

Using equation 1, $n \pmod p \times 2n \pmod p \times ... \times (p-1)n \pmod p = (p-1)!\pmod p$

$(p-1)!\pmod p \equiv (p-1)!n^{p-1}$

So $1 \pmod p \equiv n^{p-1}$

Answer 1

This is basically Dirichlet's proof of Fermat's little theorem.

Let $S=\{1, 2, \ldots, p-1\}$ be the set of residues modulo $p$. Then, $S'=\{a, 2a, \ldots, a(p-1)\}$ is also a set of residues modulo $p$ provided that $\gcd(a,p)=1$. To see this, notice that no pair $x, y$ of elements in $S'$ are equivalent modulo $p$.

Using interactively the property of congruences that $a\equiv b\pmod p\iff ca\equiv cb\pmod p$, for $\gcd(c,p)=1$, we write

$$ a^{p-1}(p-1)!\equiv(p-1)!\pmod p $$

and cancel $(p-1)!$ in both sides to conclude that

$$ a^{p-1}\equiv 1\pmod p $$