theorem Th31: :: HILB10_1:28

for n being Nat
for x, y being Integer
for a being non trivial Nat holds (sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|)