theorem Th27: :: PEPIN:27

for n, m being Nat st m mod 2 = 0 holds
(n |^ (m div 2)) ^2 = n |^ m