In the book I read there are proofs of FLT for certain cases before the common case.
When a=7, authors first write that it's possible to check all remainders of $a\mod7$, and then that it's ineffective and that $(a^7-7)\mod7$ can be represented as multiplication of seven consequent numbers (by module 7).
But before that they write something like:
As soon as every integer can be represented as $a-7b,7b \pm1,7b\pm2,7b\pm3$ it's obvious that we can check only $a=0,1,2,3 \mod 7 $
Why is it obvious?
I guess the idea is that $(-a)^7\equiv -(a^7) \pmod{7}$, and if you already know that $a^7\equiv a\pmod{7}$, then this gives $(-a)^7\equiv -(a^7)\equiv -a\pmod{7}$.
Once you've checked this works for $a=0,1,2,3$, the other values are negatives of these values, and so the above applies.
Honestly, maybe it would've been easier just to check the other three cases. :-)