theorem Th30: :: NUMBER17:30

for n being Nat holds 3 divides (2 |^ (2 * n)) - 1