theorem Th39: :: NUMBER02:39
for z being non zero Nat holds (2 |^ (2 |^ z)) mod 3 = 1