theorem :: NUMBER03:41

for n being Nat holds
( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff not 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 )