A power of five modulo nineteen

$\gcd (5,19)=1$ , so we proceed by Euler's Totient Theorem. $\phi (19)=19-1=18$ , so $400 \, \mathrm{mod} \, 18=4$ , giving us $5^4 \equiv 6^2 \equiv 36 \equiv \boxed{17} \pmod{19}$ .

Source: InternLM Lean-Workbook, record lean_workbook_53641 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.