lean_workbook_plus_74031

FLT says that for prime $p$ and $a\not\equiv0\pmod{p}$ , then we have $a^{p-1}\equiv1\pmod{p}$ . Since $10\not\equiv0\pmod{p}$ (i.e. $10$ isn't a multiple of $2017$ ), we have by FLT $10^{2016}\equiv1\pmod{2017}$ .