theorem :: NUMBER15:83
for k being non zero Nat
for x, y being positive Nat holds not ((x |^ 2) + (2 |^ (2 * k))) + 1 = y |^ 3