theorem Th24: :: NUMBER04:24

for a being odd Nat st a > 1 holds
for s being Nat st s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 holds
( (a |^ s) + 1 > s & (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 )