Metamath Blueprint : AKS (PRIMES is in P)
Theorem
aks61c5
Status:
Draft
Reference:
Claim 5 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf