theorem Th40: :: NUMBER03:40

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