theorem :: NUMBER08:108

for n being Nat
for p being Prime st n <> 0 holds
for x, y being positive Nat holds not x * (x + 1) = ((p |^ (2 * n)) * y) * (y + 1)