let a, k, l be Nat; ( k <> l & k + 1 is odd & k + 1 is prime & l + 1 is odd & l + 1 is prime implies (2 * (k + 1)) * (l + 1) divides (a |^ ((k * l) + 1)) - a )
assume that
A0:
k <> l
and
A1:
( k + 1 is odd & k + 1 is prime & l + 1 is odd & l + 1 is prime )
; (2 * (k + 1)) * (l + 1) divides (a |^ ((k * l) + 1)) - a
A2:
k + 1 <> l + 1
by A0;
( k + 1 divides (a |^ ((k * l) + 1)) - a & l + 1 divides (a |^ ((k * l) + 1)) - a )
by A1, Th73;
then A5:
(k + 1) * (l + 1) divides (a |^ ((k * l) + 1)) - a
by A1, A2, INT_2:30, PEPIN:4;
A6:
(k + 1) * (l + 1),2 |^ 1 are_coprime
by A1, NAT_5:3;
2 divides (a |^ ((1 * (k * l)) + 1)) - a
by Th74;
then
2 * ((k + 1) * (l + 1)) divides (a |^ ((k * l) + 1)) - a
by A5, A6, PEPIN:4;
hence
(2 * (k + 1)) * (l + 1) divides (a |^ ((k * l) + 1)) - a
; verum