theorem Th78: :: NEWTON02:176
for a, k, l being Nat st k <> l & k + 1 is odd & k + 1 is prime & l + 1 is odd & l + 1 is prime holds
(2 * (k + 1)) * (l + 1) divides (a |^ ((k * l) + 1)) - a