theorem Th80: :: NUMBER17:80
for s being positive Nat holds 23 divides (2 |^ (2 |^ ((10 * s) + 1))) + 19