theorem :: GAUSSINT:46

for q being G_INTEG st Norm q is Prime holds
q is g_prime