theorem Th17: :: NUMBER16:17
for n being Nat ex k being Nat st
( 17 divides k & k = ((10 |^ ((16 * n) + 9)) - 7) / 3 )