theorem Th39: :: NUMBER03:39

for n being Nat holds
( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff ( n mod 4 = 1 or n mod 4 = 2 ) )